Commit 2022-11-25 02:14 fe3cd450

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.