Theorem ContinuousLinearEquiv.symm_trans_self

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.symm_trans_selfView on Github →