Iterated matrix-vector multiplication

Multiplying a vector by a matrix twice is multiplying it by the square of the matrix, so a square-zero matrix annihilates every vector in two steps. This is the form in which the nilpotence of a root operator reaches the vector it acts on.

Main results

• TauCeti.mulVec_mulVec_eq_zero_of_pow_two_eq_zero: a square-zero matrix annihilates every vector in two multiplications.

theorem TauCeti.mulVec_mulVec_eq_zero_of_pow_two_eq_zero {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Semiring R] {M : Matrix n n R} (hM : M ^ 2 = 0) (v : n → R) : M.mulVec (M.mulVec v) = 0

A square-zero matrix annihilates every vector in two multiplications.