oriented_angle): angles equal to 0 or π (#16229)

Commit

3 years ago

feat(geometry/euclidean/oriented_angle): angles equal to 0 or π (#16229) Add lemmas about various conditions for oriented angles between two vectors to equal 0 or π.

Author

jsm28

Parents

a51c2fd2

mathlib f1f166b2 - feat(geometry/euclidean/oriented_angle): angles equal to 0 or π (#16229)

mathlib
f1f166b2 - feat(geometry/euclidean/oriented_angle): angles equal to 0 or π (#16229)