2025-12-23 00:20
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
chore(Analysis/Normed/Operator/LinearIsometry): change coercion for `LinearIsometryEquiv.toContinuousLinearEquiv` (#32964) …
Added LinearIsometryEquiv.toContinuousLinearEquiv_trans