Mathlib v3 is deprecated. Go to Mathlib v4

Theorem affine.simplex.orthogonal_projection_vadd_smul_vsub_orthogonal_projection

Modification history

2022-02-24 11:57
src/geometry/euclidean/circumcenter.lean
chore(geometry/euclidean): split repetitive proof (#12209) …
Added affine.simplex.orthogonal_projection_vadd_smul_vsub_orthogonal_projectionView on Github →