Theorem ContinuousLinearMap.IsStarNormal.ker_adjoint_eq_ker

Modification history

2025-09-09 15:52
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
feat(Analysis/InnerProductSpace/Adjoint): `(range T)ᗮ = ker T` for normal operators (#29384)
Added ContinuousLinearMap.IsStarNormal.ker_adjoint_eq_kerView on Github →