Commit 2025-03-31 10:57 ac505701
View on Github →feat(Geometry/Euclidean/Basic): orthogonal projection onto singleton (#23323) Add the lemma:
@[simp] lemma orthogonalProjection_affineSpan_singleton (p₁ p₂ : P) :
orthogonalProjection (affineSpan ℝ {p₁}) p₂ = p₁ := by