feat(geometry/euclidean/oriented_angle): angles equal to 0 or π (#16229)
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 π.







leanprover-community/mathlib,leanprover-community/mathlib