feat: {Continuous}Linear{Isometry}Equiv.conj{Continuous, Star}AlgEquiv are "almost" injective

[themathqueen]

... "almost" meaning that they are colinear. I.e., f.conj{Continuous, Star}AlgEquiv S = g.conj{Continuous, Star}AlgEquiv S iff f = α • g for some (unitary) α.

Also, the same for Unitary.conjStarAlgAut. All in one PR since they all have analogous proofs.

---

• depends on: [Merged by Bors] - chore(Algebra/Central/End): generalize Algebra.IsCentral.instEnd #33301

[github-actions]

PR summary ce5b0921e0

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.InnerProductSpace.Adjoint	1983	1992	+9 (+0.45%)
Mathlib.Algebra.Star.UnitaryStarAlgAut	863	866	+3 (+0.35%)
Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv	2076	2077	+1 (+0.05%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv	1
3 files Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Probability.Distributions.Gaussian.CharFun Mathlib.Probability.Moments.CovarianceBilin	2
Mathlib.Algebra.Star.UnitaryStarAlgAut	3
Mathlib.Analysis.Convex.Cone.InnerDual	4
4 files Mathlib.Analysis.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.Matrix.Order Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus	7
4 files Mathlib.Analysis.Matrix.LDL Mathlib.Analysis.Matrix.PosDef Mathlib.Analysis.Matrix.Spectrum Mathlib.LinearAlgebra.Matrix.LDL	8
15 files Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Convex.DoublyStochasticMatrix Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.TensorProduct Mathlib.Analysis.InnerProductSpace.Trace Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.Matrix.Swap	9

---

Declarations diff

+ conjStarAlgAut_ext_iff
+ conjStarAlgAut_ext_iff'
+ conjStarAlgAut_symm_unitaryLinearIsometryEquiv
+ conjStarAlgEquiv_ext_iff
+ conjStarAlgEquiv_unitaryLinearIsometryEquiv
+ eq_toContinuousLinearMap_symm_comp
+ instance : SMul (unitary 𝕜) (V ≃ₗᵢ[𝕜] W) where smul α e
+ instance : SMul Sˣ (V ≃L[R] W) where smul α e
+ instance : SMul Sˣ (V ≃ₗ[R] W) where smul α e
+ symm_units_smul
+ toContinuousLinearEquiv_smul
+ toLinearMap_smul
++ symm_smul
++ toLinearEquiv_smul
+++ smul_apply
+++ smul_trans
+++ symm_smul_apply
+++ trans_smul

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(Algebra/Central/End): generalize Algebra.IsCentral.instEnd #33301
  By Dependent Issues (🤖). Happy coding!

[themathqueen]

Stating this in terms of LinearEquiv instead of bare functions would make this less general since it would require GroupWithZero for Units.mk0. Unless there's an alternate proof I'm not thinking of?

See below for the stronger one (but with the nicer statement). Which one should I remove?

[themathqueen]

Same here. This is stronger, but with a nicer statement. Which should I remove?