Mathlib v3 is deprecated. Go to Mathlib v4

Theorem euclidean_geometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter

Modification history

2020-10-06 12:41
src/geometry/euclidean/monge_point.lean
feat(geometry/euclidean/monge_point): orthocentric systems (#4448) …
Added euclidean_geometry.exists_dist_eq_circumradius_of_subset_insert_orthocenterView on Github →