Commit 2025-12-30 23:52 c6513d00

View on Github →

feat(Analysis/Normed/Operator): star-algebra equivalences between continuous endomorphisms are isometrically inner (#33066) This is the star-algebra equivalence version of AlgEquiv.eq_linearEquivConjAlgEquiv and ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv. So we now have a characterization of algebra, continuous algebra, and star-algebra equivalences between endomorphisms. The proof follows the same idea as the one in #28972.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

added def LinearIsometryEquiv.conjStarAlgEquiv

added theorem LinearIsometryEquiv.conjStarAlgEquiv_apply

added theorem LinearIsometryEquiv.conjStarAlgEquiv_apply_apply

added theorem LinearIsometryEquiv.conjStarAlgEquiv_refl

added theorem LinearIsometryEquiv.conjStarAlgEquiv_trans

added theorem LinearIsometryEquiv.symm_conjStarAlgEquiv

added theorem LinearIsometryEquiv.symm_conjStarAlgEquiv_apply_apply

Modified Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean

added theorem coe_auxContinuousLinearEquiv

added theorem coe_auxIsometry

added theorem coe_symm_auxIsometry

Modified Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean

Modified Mathlib/Topology/Algebra/Algebra/Equiv.lean

added theorem ContinuousAlgEquiv.coe_mk