Theorem orthogonalProjection_eq_zero_iff

Modification history

2025-04-22 07:21

Mathlib/Analysis/InnerProductSpace/Projection.lean

chore: rename `orthogonalProjection` to `Submodule.orthogonalProjection` (#24247) …

Deleted orthogonalProjection_eq_zero_iff View on Github →

2023-09-04 08:29

Mathlib/Analysis/InnerProductSpace/Projection.lean

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

Added orthogonalProjection_eq_zero_iff View on Github →