Commit 2022-07-18 08:07 e3f47f2b
View on Github →feat(geometry/euclidean/oriented_angle): continuous_at_oangle
(#15463)
Add lemmas that oriented angles are continuous, as a function of a
pair of vectors, except where one of the vectors is zero, analogous to
the lemmas previously added for unoriented angles.