Commit 2025-12-27 18:47 d9996c5f

View on Github →

feat(Analysis/Normed/Operator): continuous algebra equivalences between continuous endomorphisms are inner (#33017) This is the continuous version of AlgEquiv.eq_linearEquivConjAlgEquiv. The proof follows the same idea as the non-continuous version.

Estimated changes

Modified Mathlib.lean

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

Modified Mathlib/Topology/Algebra/Algebra.lean

added theorem ContinuousAlgHom.coe_toContinuousLinearMap

added def ContinuousAlgHom.toContinuousLinearMap

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

added theorem ContinuousLinearEquiv.eq_comp_toContinuousLinearMap_symm

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

added def ContinuousLinearEquiv.conjContinuousAlgEquiv

added theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_apply

added theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply

added theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_refl

added theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_trans

added theorem ContinuousLinearEquiv.symm_conjContinuousAlgEquiv

added theorem ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply