Theorem LinearIsometryEquiv.toContinuousLinearEquiv_refl

Modification history

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_refl View on Github →