Commit 2023-09-04 08:29 01fd4ae9

View on Github →

feat: kernel of orthogonalProjection K is Kᗮ (#6943)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

added theorem ker_orthogonalProjection

added theorem orthogonalProjection_eq_zero_iff