Divisibility of matrix entries under multiplication

A common divisor of the entries of a matrix survives multiplication on either side: every entry of P * A * Q is an S-combination of entries of A, so anything dividing all of those divides all of these.

Nothing here needs invertibility, a square shape, or a diagonal target — only that the products are conformable — so the statements are at NonUnitalCommSemiring and rectangular. No multiplicative identity is involved; multiplication is used both associatively and commutatively.

The Smith-normal-form theory consumes both, but neither has a Smith-normal-form hypothesis and neither should require importing that theory to reach.

Main results

• Matrix.dvd_mul_mul_apply: a common divisor of the entries of A divides every entry of P * A * Q.
• Matrix.dvd_diag_of_dvd_entries: if L * A * R is Matrix.diagonal d, then a common divisor of the entries of A divides every d k.
• Matrix.forall_dvd_apply_iff_of_mul_eq_mul: if W * B = A * W, then an element coprime to det W divides every entry of A exactly when it divides every entry of B — A and B are conjugate after inverting det W.

theorem Matrix.dvd_mul_mul_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {S : Type u_5} [NonUnitalCommSemiring S] [Fintype m] [Fintype n] {A : Matrix m n S} {c : S} (hc : ∀ (i : m) (j : n), c ∣ A i j) (P : Matrix l m S) (Q : Matrix n o S) (i : l) (j : o) : c ∣ (P * A * Q) i j

A common divisor of the entries survives two-sided multiplication. If c divides every entry of A, then it divides every entry of P * A * Q, since each entry of the product is an S-combination of entries of A.

theorem Matrix.dvd_diag_of_dvd_entries {m : Type u_2} {n : Type u_3} {o : Type u_4} {S : Type u_5} [NonUnitalCommSemiring S] [Fintype m] [Fintype n] [DecidableEq o] (A : Matrix m n S) (c : S) (d : o → S) (L : Matrix o m S) (R : Matrix n o S) (h : L * A * R = diagonal d) (hc : ∀ (i : m) (j : n), c ∣ A i j) (k : o) : c ∣ d k

Every common divisor of the entries divides every diagonal entry. Each d k is the (k, k) entry of L * A * R, hence an S-combination of the entries of A.

theorem Matrix.forall_dvd_apply_iff_of_mul_eq_mul {n : Type u_3} {R : Type u_6} [CommRing R] [Fintype n] [DecidableEq n] {A B W : Matrix n n R} (h : W * B = A * W) {e : R} (he : IsCoprime e W.det) : (∀ (i j : n), e ∣ A i j) ↔ ∀ (i j : n), e ∣ B i j

Conjugation by a matrix of determinant coprime to e preserves divisibility by e. If W * B = A * W, then adjugate W * A * W = det W • B and W * B * adjugate W = det W • A, so an e coprime to det W divides every entry of A exactly when it divides every entry of B.