mathlib

f8b900bf - refactor(geometry/euclidean): split up unoriented angles (#16942)

refactor(geometry/euclidean): split up unoriented angles (#16942) Move the definitions and lemmas about unoriented angles from `geometry.euclidean.basic` (quite a large file) to new `geometry.euclidean.angle.unoriented.basic` and `geometry.euclidean.angle.unoriented.affine`. Also move some lemmas about right-angled triangles from `geometry.euclidean.triangle` to `geometry.euclidean.angle.unoriented.right_angle` (there's not much there at present, but I expect to add lots of lemmas about trigonometric functions of angles in right-angled triangles, which should be enough to justify having a separate file for such content). I expect to split up `geometry.euclidean.oriented_angle` similarly, into files under `geometry.euclidean.angle.oriented`, once Heather's refactor is in. When it becomes convenient to deduce results about unoriented angles from those about oriented angles rather than vice versa, as with circle theorems, I expect to put such groups of results in e.g. `geometry.euclidean.angle.sphere` rather than in separate unoriented and oriented files. Although not done here, dependencies could be reduced further by moving two lemmas about conformal maps from `geometry.euclidean.angle.unoriented.basic` to a separate `geometry.euclidean.angle.unoriented.conformal` (most uses of angles don't need `analysis.calculus.conformal.normed_space`). There are no changes to lemma statements or proofs.