Properties of ZMod residues

Elementary properties of finite residues ZMod m for [NeZero m]: valuation preservation under ZMod.finEquiv, residue subtraction on values without truncated subtraction below zero, and equivalence of list range sums with residue sums.

Main results

• ZMod.val_finEquiv: valuation preservation under ZMod.finEquiv.
• ZMod.val_finEquiv_symm: valuation preservation under (ZMod.finEquiv m).symm.
• ZMod.val_sub_eq_mod: residue subtraction on values.
• ZMod.sum_range_eq_sum_zmod: a sum over List.range m is a sum over ZMod m.

theorem ZMod.val_finEquiv {m : ℕ} [NeZero m] (i : Fin m) : ((finEquiv m) i).val = ↑i

Valuation is preserved under the ring equivalence ZMod.finEquiv.

theorem ZMod.val_finEquiv_symm {m : ℕ} [NeZero m] (z : ZMod m) : ↑((finEquiv m).symm z) = z.val

(ZMod.finEquiv m).symm preserves the underlying natural-number value.

theorem ZMod.sum_range_eq_sum_zmod {A : Type u_1} [AddCommMonoid A] (m : ℕ) [NeZero m] (f : ℕ → A) : (List.map f (List.range m)).sum = ∑ z : ZMod m, f z.val

A sum over List.range m is a sum over the residues modulo m.

theorem ZMod.val_sub_eq_mod {m : ℕ} [NeZero m] (u v : ZMod m) : (u - v).val = (u.val + m - v.val) % m

Residue subtraction on values, without truncated subtraction below zero.