feat: port Geometry.Euclidean.Angle.Unoriented.Basic (#4376)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
leanprover-community · May 26, 2023 · 1220050 · 1220050
1 parent 23c0f40
commit 1220050
Show file tree

Hide file tree

Showing 2 changed files with 378 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1489,6 +1489,7 @@ import Mathlib.FieldTheory.Separable
 import Mathlib.FieldTheory.SeparableDegree
 import Mathlib.FieldTheory.Subfield
 import Mathlib.FieldTheory.Tower
+import Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
 import Mathlib.Geometry.Euclidean.Inversion
 import Mathlib.Geometry.Manifold.ChartedSpace
 import Mathlib.Geometry.Manifold.ConformalGroupoid