Theorem Unitary.coe_symm_linearIsometryEquiv_apply

Modification history

2025-12-23 00:20
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
chore(Analysis/Normed/Operator/LinearIsometry): change coercion for `LinearIsometryEquiv.toContinuousLinearEquiv` (#32964) …
Added Unitary.coe_symm_linearIsometryEquiv_applyView on Github →