feat: port Geometry.Euclidean.MongePoint (#5056)

Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
leanprover-community · Jun 28, 2023 · ef7e7c0 · ef7e7c0
1 parent 449de62
commit ef7e7c0
Show file tree

Hide file tree

Showing 2 changed files with 801 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1835,6 +1835,7 @@ import Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
 import Mathlib.Geometry.Euclidean.Basic
 import Mathlib.Geometry.Euclidean.Circumcenter
 import Mathlib.Geometry.Euclidean.Inversion
+import Mathlib.Geometry.Euclidean.MongePoint
 import Mathlib.Geometry.Euclidean.Sphere.Basic
 import Mathlib.Geometry.Euclidean.Sphere.Power
 import Mathlib.Geometry.Euclidean.Sphere.Ptolemy