Theorem LinearIsometryEquiv.conjStarAlgEquiv_refl

Modification history

2026-06-16 09:46
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
feat: expand API for `StarAlgEquiv` (#40517) …
Modified LinearIsometryEquiv.conjStarAlgEquiv_reflView on Github →
2025-12-30 23:52
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
feat(Analysis/Normed/Operator): star-algebra equivalences between continuous endomorphisms are isometrically inner (#33066) …
Added LinearIsometryEquiv.conjStarAlgEquiv_reflView on Github →