Def EuclideanGeometry.orthogonalProjection

Modification history

2025-12-11 08:08

Mathlib/Geometry/Euclidean/Projection.lean

refactor(Geometry/Euclidean/Projection): redefine projection and reflection for affine subspaces (#27378) …

Added EuclideanGeometry.orthogonalProjection View on Github →