mathlib3

34d8782b - feat(geometry/euclidean/angle/oriented/basic): `inner_eq_zero` lemmas (#17265)

feat(geometry/euclidean/angle/oriented/basic): `inner_eq_zero` lemmas (#17265) Add various lemmas relating an inner product of zero between two vectors to the oriented angle between those vectors.