Commit 2025-12-23 00:20 9fdb8ee7

View on Github →

chore(Analysis/Normed/Operator/LinearIsometry): change coercion for LinearIsometryEquiv.toContinuousLinearEquiv (#32964) Currently, including the type (e : E →SL[σ₁₂] E₂) for a linear isometry equivalence e looks messy in the infoview and docs. So we change the coercion of (e : _ ≃SL _) to go through e.toContinuousLinearEquiv.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

added theorem Unitary.coe_linearIsometryEquiv_apply

added theorem Unitary.coe_symm_linearIsometryEquiv_apply

deleted theorem Unitary.linearIsometryEquiv_coe_apply

deleted theorem Unitary.linearIsometryEquiv_coe_symm_apply

Modified Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean

Modified Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

modified theorem LinearIsometryEquiv.coe_coe''

modified theorem LinearIsometryEquiv.coe_coe

added theorem LinearIsometryEquiv.toContinuousLinearEquiv_refl

added theorem LinearIsometryEquiv.toContinuousLinearEquiv_trans

added theorem LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

added theorem ContinuousLinearEquiv.self_trans_symm

added theorem ContinuousLinearEquiv.symm_trans_self