Divisibility read off congruences modulo n

Facts about integers read off congruences in ZMod n, and divisibility inside the ring ZMod n itself.

A linear congruence with unit coefficient is solvable: if b is a unit modulo n, then some residue j : ZMod n satisfies n ∣ a - j.val * b over ℤ. The solution is j = a b⁻¹, and it is returned as a residue class together with its canonical representative j.val, which is the form a coset representative indexed by Fin n needs.

ZMod.exists_dvd_sub_val_mul was extracted from TauCeti/NumberTheory/ModularForms/CongruenceSubgroups.lean, where it was private; that index calculation was ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/CongruenceIndex.lean, Chris Birkbeck, Apache-2.0). The lemma is consumed there and in HeckeRing/GL2/Gamma1/CoprimeCosets.lean.

ZMod.natCast_dvd_val_sub_of_unitsMap_eq is adapted from the same project (Chris Birkbeck, github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 2baa76f74, file projects/LeanModularForms/LeanModularForms/Eigenforms/ConductorTheorem.lean, declaration natCast_val_sub_dvd_of_unitsMap_eq (:665). Two departures from the source: it is stated for an arbitrary divisor d ∣ N rather than only for the reduction modulo N / l, which is all its proof uses, and the name places the divisibility in Mathlib's operand order.

Main results

• ZMod.exists_dvd_sub_val_mul: the congruence j b ≡ a (mod n) has a solution j : ZMod n whenever b is a unit modulo n.
• ZMod.natCast_dvd_val_sub_of_unitsMap_eq: two units with the same image under ZMod.unitsMap along d ∣ N have representatives congruent modulo d, as integers.
• ZMod.intCast_lcm_eq_of_eq_of_eq: one residue modulo lcm a b from the residues modulo a and b — the Chinese remainder theorem for a single integer.
• ZMod.natCast_natAbs_eq_of_mul_nonneg: congruent integers with nonnegative product have congruent absolute values.
• ZMod.eq_of_forall_cast_eq_of_prime_pow_dvd: a residue modulo n is determined by its reductions modulo the prime powers dividing n.
• ZMod.equivPi_apply: the components of Mathlib's Chinese remainder isomorphism ZMod.equivPi are the reductions modulo the prime powers exactly dividing n.
• ZMod.dvd_of_forall_mul_eq_zero: divisibility inside ZMod n from annihilators: if every r with r d = 0 has r x = 0, then d ∣ x.

theorem ZMod.exists_dvd_sub_val_mul (n : ℕ) [NeZero n] (a b : ℤ) (hb : IsUnit ↑b) : ∃ (j : ZMod n), ↑n ∣ a - ↑j.val * b

A linear congruence with unit coefficient is solvable. If b is a unit modulo n, then n ∣ a - j.val * b for some j : ZMod n, namely j = a b⁻¹.

theorem ZMod.natCast_dvd_val_sub_of_unitsMap_eq {N : ℕ} [NeZero N] {d : ℕ} (hd : d ∣ N) (u u' : (ZMod N)ˣ) (h_eq : (unitsMap hd) u = (unitsMap hd) u') : ↑d ∣ ↑(↑u).val - ↑(↑u').val

From equal reductions to an integer congruence. Two units with the same image under the reduction (ZMod N)ˣ → (ZMod d)ˣ along d ∣ N have representatives congruent modulo d, as integers. This is the bridge from unit bookkeeping to statements about integer matrix entries.

theorem ZMod.intCast_lcm_eq_of_eq_of_eq {a b : ℕ} {x y : ℤ} (ha : ↑x = ↑y) (hb : ↑x = ↑y) : ↑x = ↑y

One residue modulo a least common multiple from the residues modulo the two moduli: the Chinese remainder theorem Int.modEq_and_modEq_iff_modEq_lcm, read in ZMod.

theorem ZMod.natCast_natAbs_eq_of_mul_nonneg {m : ℕ} {z w : ℤ} (hzw : 0 ≤ z * w) (h : ↑z = ↑w) : ↑z.natAbs = ↑w.natAbs

Congruent integers with nonnegative product have congruent absolute values. If z * w ≥ 0 and z ≡ w modulo m, then |z| ≡ |w| modulo m.

theorem ZMod.eq_of_forall_cast_eq_of_prime_pow_dvd {n : ℕ} [NeZero n] {x y : ZMod n} (h : ∀ (p k : ℕ), Nat.Prime p → k ≠ 0 → p ^ k ∣ n → x.cast = y.cast) : x = y

A residue is determined by its reductions modulo prime powers. Two residues modulo n whose reductions modulo every prime power p ^ k dividing n agree are equal: the Chinese remainder theorem in its uniqueness form, along the prime factorization of n.

@[simp]

theorem ZMod.equivPi_apply (n : ℕ) (hn : n ≠ 0) (x : ZMod n) (p : ↥n.primeFactors) : (equivPi n hn) x p = (castHom ⋯ (ZMod (↑p ^ n.factorization ↑p))) x

The component at p of the Chinese remainder isomorphism ZMod.equivPi is reduction modulo p ^ n.factorization p.

theorem ZMod.dvd_of_forall_mul_eq_zero {n : ℕ} [NeZero n] {d x : ZMod n} (h : ∀ (r : ZMod n), r * d = 0 → r * x = 0) : d ∣ x

Divisibility in ℤ/nℤ from annihilators. If every r : ZMod n with r * d = 0 also has r * x = 0, then d ∣ x. With g = gcd(d, n), the element n / g kills d, hence x, so g divides x; and g = d * d⁻¹ is a multiple of d in ZMod n (ZMod.mul_inv_eq_gcd).