Commit 2026-05-11 19:07 eab0863f

View on Github →

feat(Analysis): LinearMap.id is unitary (#39066) This is for simp. From MeanFourier

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

modified theorem ContinuousLinearMap.adjoint_id

added theorem ContinuousLinearMap.adjoint_one

added theorem ContinuousLinearMap.id_mem_unitary

modified theorem LinearMap.adjoint_id

added theorem LinearMap.adjoint_one

added theorem LinearMap.id_mem_unitary

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean