Commit 2022-10-13 06:01 f8b900bf

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.