Parity of the diagonal of a symmetric integer matrix

For a symmetric integer matrix A and an integer vector m, the quadratic form mᵀ A m = ∑ᵢⱼ mᵢ mⱼ aᵢⱼ agrees modulo two with ∑ᵢ mᵢ aᵢᵢ: its off-diagonal part is even because the summand is symmetric under swapping the indices, and mᵢ² ≡ mᵢ modulo two. In particular ∑ᵢ mᵢ aᵢᵢ is even whenever mᵀ A m = 0, for instance whenever A m = 0.

Main results

• Matrix.IsSymm.even_sum_mul_diag_iff_even_dotProduct_mulVec: if A is a symmetric integer matrix then ∑ᵢ mᵢ aᵢᵢ is even if and only if mᵀ A m is.
• Matrix.IsSymm.even_sum_mul_diag_of_dotProduct_mulVec_eq_zero: if A is a symmetric integer matrix and mᵀ A m = 0, then ∑ᵢ mᵢ aᵢᵢ is even.

theorem Matrix.IsSymm.even_sum_mul_diag_iff_even_dotProduct_mulVec {ι : Type u_1} [Fintype ι] {A : Matrix ι ι ℤ} (hA : A.IsSymm) (m : ι → ℤ) : Even (∑ i : ι, m i * A i i) ↔ Even (m ⬝ᵥ A.mulVec m)

If A is a symmetric integer matrix and m is an integer vector, then ∑ᵢ mᵢ aᵢᵢ has the same parity as the quadratic form mᵀ A m. The individual terms mᵢ aᵢᵢ need not be even.

theorem Matrix.IsSymm.even_sum_mul_diag_of_dotProduct_mulVec_eq_zero {ι : Type u_1} [Fintype ι] {A : Matrix ι ι ℤ} (hA : A.IsSymm) {m : ι → ℤ} (hm : m ⬝ᵥ A.mulVec m = 0) : Even (∑ i : ι, m i * A i i)

If A is a symmetric integer matrix and m is an integer vector with mᵀ A m = 0, then ∑ᵢ mᵢ aᵢᵢ is even. The individual terms mᵢ aᵢᵢ need not be even.