Theorem ContinuousAlgEquiv.coe_mk

Modification history

2025-12-30 23:52
Mathlib/Topology/Algebra/Algebra/Equiv.lean
feat(Analysis/Normed/Operator): star-algebra equivalences between continuous endomorphisms are isometrically inner (#33066) …
Added ContinuousAlgEquiv.coe_mkView on Github →