Counting residues by a condition on their reduction

A condition on x : ZMod n that only reads the reduction of x modulo a divisor of n can be counted after reducing. This file records the two counting laws that result.

Reducing along a single divisor m ∣ n multiplies the count: the reduction ZMod n → ZMod m, written here as fun x ↦ (x.val : ZMod m), is a surjective additive homomorphism, so all of its fibres have the same size and a condition pulled back along it holds proportionally often. The identity is stated as m * (count over ZMod n) = n * (count over ZMod m), which carries the same information as a division by m without a quotient appearing.

Splitting a modulus into pairwise coprime factors multiplies the counts: conditions imposed on the separate factors are independent, so the number of residues satisfying all of them is the product of the individual counts. This is the Chinese remainder theorem ZMod.prodEquivPi in counting form.

Main results

• ZMod.mul_card_filter_natCast_val: counting a condition on the reduction modulo m ∣ n.
• ZMod.card_filter_forall_natCast_val: counting independent conditions on coprime factors.
• ZMod.card_filter_not_self_dvd_val: the residues whose representative the modulus does not divide, the base case of such a count.

theorem ZMod.mul_card_filter_natCast_val {m n : ℕ} [NeZero m] [NeZero n] (hmn : m ∣ n) (Q : ZMod m → Prop) [DecidablePred Q] : m * {x : ZMod n | Q ↑x.val}.card = n * {y : ZMod m | Q y}.card

Counting a condition on the reduction modulo a divisor. For m ∣ n, the residues modulo n whose reduction modulo m satisfies Q are n / m times as many as the residues modulo m satisfying Q, stated without the quotient.

@[simp]

theorem ZMod.card_filter_not_self_dvd_val {m : ℕ} [NeZero m] : {z : ZMod m | ¬m ∣ z.val}.card = m - 1

All residues but zero have a representative the modulus does not divide. A representative is smaller than the modulus, so the modulus divides it exactly when it vanishes.

theorem ZMod.card_filter_forall_natCast_val {ι : Type u_1} [Fintype ι] (a : ι → ℕ) (hcop : Pairwise (Function.onFun Nat.Coprime a)) [∀ (i : ι), NeZero (a i)] [NeZero (∏ i : ι, a i)] (Q : (i : ι) → ZMod (a i) → Prop) [(i : ι) → DecidablePred (Q i)] : {x : ZMod (∏ i : ι, a i) | ∀ (i : ι), Q i ↑x.val}.card = ∏ i : ι, {y : ZMod (a i) | Q i y}.card

Counting independent conditions on coprime factors. If the moduli a i are pairwise coprime, the residues modulo ∏ i, a i whose reduction modulo each a i satisfies Q i are counted by the product over i of the residues modulo a i satisfying Q i.