Commit 2025-09-09 15:52 70ddb5d1

View on Github →

feat(Analysis/InnerProductSpace/Adjoint): (range T)ᗮ = ker T for normal operators (#29384)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

added theorem ContinuousLinearMap.IsStarNormal.adjoint_apply_eq_zero_iff

added theorem ContinuousLinearMap.IsStarNormal.ker_adjoint_eq_ker

added theorem ContinuousLinearMap.IsStarNormal.orthogonal_range

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean