Theorem Affine.Simplex.dist_orthogonalProjection_faceOpposite_pos

Modification history

2025-05-01 21:43
Mathlib/Geometry/Euclidean/Projection.lean
feat(Geometry/Euclidean/Altitude): `altitudeFoot`, `height` (#24525) …
Deleted Affine.Simplex.dist_orthogonalProjection_faceOpposite_posView on Github →
2025-04-26 15:45
Mathlib/Geometry/Euclidean/Basic.lean
refactor(Geometry/Euclidean/Projection): split out orthogonal projections (#24389) …
Modified Affine.Simplex.dist_orthogonalProjection_faceOpposite_posView on Github →
2025-04-07 07:19
Mathlib/Geometry/Euclidean/Basic.lean
feat(Geometry/Euclidean/Basic): projection of vertex to opposite face of simplex (#23712) …
Added Affine.Simplex.dist_orthogonalProjection_faceOpposite_posView on Github →