mathlib

fe3cd450 - feat(geometry/euclidean/angle/oriented/basic): `π / 2` rotations and inner product (#17687)

feat(geometry/euclidean/angle/oriented/basic): `π / 2` rotations and inner product (#17687) Add a series of lemmas relating to the inner product of a vector and a `π / 2` rotation of that vector being zero, with variants that are convenient for `simp` and an `iff` lemma that the inner product is zero if and only if a vector is zero or one is a multiple of a `π / 2` rotation of the other.