refactor(geometry/euclidean/angle/oriented/basic): split out rotations (

#18212) `geometry.euclidean.angle.oriented.basic` is 1489 lines long. Reduce it to 1032 lines by splitting out the definition of and results about `rotation` to a separate file. (No results in this file involve `rotation` in their proofs unless it's also involved in the statement.) There are no changes to API or proofs.
leanprover-community · Jan 18, 2023 · fb31989 · fb31989
1 parent df78eae
commit fb31989
Show file tree

Hide file tree

Showing 3 changed files with 489 additions and 458 deletions.
diff --git a/src/geometry/euclidean/angle/oriented/affine.lean b/src/geometry/euclidean/angle/oriented/affine.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
 import analysis.convex.side
-import geometry.euclidean.angle.oriented.basic
+import geometry.euclidean.angle.oriented.rotation
 import geometry.euclidean.angle.unoriented.affine
 
 /-!