feat: port Geometry.Euclidean.Angle.Oriented.Affine (#5016)

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
leanprover-community · Jun 14, 2023 · 65535ab · 65535ab
1 parent 4167cba
commit 65535ab
Show file tree

Hide file tree

Showing 2 changed files with 844 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1737,6 +1737,7 @@ import Mathlib.FieldTheory.SeparableDegree
 import Mathlib.FieldTheory.SplittingField.IsSplittingField
 import Mathlib.FieldTheory.Subfield
 import Mathlib.FieldTheory.Tower
+import Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
 import Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
 import Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
 import Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine