Theorem ker_orthogonalProjection

Modification history

2025-04-22 07:21

Mathlib/Analysis/InnerProductSpace/Projection.lean

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

Deleted ker_orthogonalProjection View on Github →

2023-09-04 08:29

Mathlib/Analysis/InnerProductSpace/Projection.lean

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

Added ker_orthogonalProjection View on Github →