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

Estimated changes