Theorem LinearIsometryEquiv.coe_coe

Modification history

2025-12-23 00:20
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
chore(Analysis/Normed/Operator/LinearIsometry): change coercion for `LinearIsometryEquiv.toContinuousLinearEquiv` (#32964) …
Modified LinearIsometryEquiv.coe_coeView on Github →
2023-04-25 11:42
Mathlib/Analysis/NormedSpace/LinearIsometry.lean
feat: port Analysis.NormedSpace.LinearIsometry (#3289)
Added LinearIsometryEquiv.coe_coeView on Github →