Commit 2024-03-07 15:45 938e7b1c

View on Github →

feat: unitary operators on a Hilbert space coincide with linear isometric equivalences (#10858) This constructs a group isomorphism unitary (H →L[𝕜] H) ≃⋆ (H ≃ₗᵢ[𝕜] H) where H is a Hilbert space. In addition, several lemmas are provided for convenience concerning unitary operators.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

added theorem ContinuousLinearMap.inner_map_map_iff_adjoint_comp_self

added theorem ContinuousLinearMap.inner_map_map_of_mem_unitary

added theorem ContinuousLinearMap.norm_map_iff_adjoint_comp_self

added theorem ContinuousLinearMap.norm_map_of_mem_unitary

added theorem LinearIsometryEquiv.adjoint_eq_symm

added theorem LinearIsometryEquiv.star_eq_symm

added theorem unitary.inner_map_map

added theorem unitary.linearIsometryEquiv_coe_apply

added theorem unitary.linearIsometryEquiv_coe_symm_apply

added theorem unitary.norm_map

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

added theorem LinearMap.norm_map_iff_inner_map_map