mathlib
54d1f9bb - refactor(geometry/euclidean/oriented_angle): split file (#17134)

Commit
3 years ago
refactor(geometry/euclidean/oriented_angle): split file (#17134) Split `geometry.euclidean.oriented_angle` up into `geometry.euclidean.angle.oriented.basic`, `geometry.euclidean.angle.oriented.affine` and `geometry.euclidean.angle.sphere` (the last only has a few results at present but is intended to get a lot more, both oriented results and unoriented results deduced from the oriented ones).
Author
Parents
Loading