mathlib

fb319896 - refactor(geometry/euclidean/angle/oriented/basic): split out rotations (#18212)

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.