Theorem ContinuousLinearMap.adjoint_one

Modification history

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