Mathlib v3 is deprecated. Go to Mathlib v4

Theorem affine.simplex.dist_sq_eq_dist_orthogonal_projection_sq_add_dist_orthogonal_projection_sq

Modification history

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