Theorem ContinuousLinearEquiv.self_trans_symm

Modification history

2025-12-23 00:20
Mathlib/Topology/Algebra/Module/Equiv.lean
chore(Analysis/Normed/Operator/LinearIsometry): change coercion for `LinearIsometryEquiv.toContinuousLinearEquiv` (#32964) …
Added ContinuousLinearEquiv.self_trans_symmView on Github →