Plane rotations with nonzero entries

A point (c, s) of the unit circle in a commutative ring gives the plane rotation !![c, -s; s, c], an orthogonal matrix. Extended by the identity it is an orthogonal n × n matrix for every n ≥ 2 whose first row has the entries c and -s. So as soon as c * s ≠ 0 there is an orthogonal matrix A and labels a ≠ b with A a a * A a b ≠ 0: an orthogonal matrix that is not a signed permutation matrix.

Main results

• TauCeti.exists_orthogonal_apply_mul_apply_ne_zero: such an orthogonal matrix exists.

theorem TauCeti.exists_orthogonal_apply_mul_apply_ne_zero {R : Type u_1} [CommRing R] {n : ℕ} (hn : 2 ≤ n) (hrot : ∃ (c : R) (s : R), c ^ 2 + s ^ 2 = 1 ∧ c * s ≠ 0) : ∃ (A : Matrix (Fin n) (Fin n) R), A.transpose * A = 1 ∧ ∃ (a : Fin n) (b : Fin n), a ≠ b ∧ A a a * A a b ≠ 0

In dimension at least two, a plane rotation through c and s is an orthogonal matrix with A a a * A a b ≠ 0 for two distinct labels a and b, as soon as c * s ≠ 0.