Theorem ContinuousLinearMap.id_mem_unitary

Modification history

2026-05-11 19:07
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
feat(Analysis): `LinearMap.id` is unitary (#39066) …
Added ContinuousLinearMap.id_mem_unitaryView on Github →