Integer matrices acting on vectors modulo a prime-power factor

If p is odd and prime to the determinant of an integer matrix A, then 2 A is invertible modulo p. Hence, in ZMod N with p * M * p = N, a vector x killed by 2 * (p * M) after applying A is already killed by p * M: both conditions say that x vanishes modulo p.

Main results

• Matrix.natCast_mul_smul_eq_zero_of_two_smul_mulVec_eq_zero: this cancellation of 2 A.

theorem Matrix.natCast_mul_smul_eq_zero_of_two_smul_mulVec_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι ℤ} {N M p : ℕ} [NeZero (p * M)] (hpM : p * M * p = N) (hodd : Odd p) (hdet : IsCoprime A.det ↑p) (x : ι → ZMod N) : (2 * ↑(p * M)) • (A.map Int.cast).mulVec x = 0 → ↑(p * M) • x = 0

Killing the 2 A-image. If p is odd and prime to det A, then in ZMod N with p * M * p = N, the vanishing of (2 * (p * M)) • (A x) forces (p * M) • x = 0: both say that x vanishes modulo p, since 2 A is invertible modulo p.