Integers mod n

Definition of the integers mod n, and the field structure on the integers mod p.

Definitions

• ZMod n, which is for integers modulo a nat n : ℕ

• val a is defined as a natural number:

  • for a : ZMod 0 it is the absolute value of a
  • for a : ZMod n with 0 < n it is the least natural number in the equivalence class

• A coercion cast is defined from ZMod n into any ring. This is a ring hom if the ring has characteristic dividing n

instance ZMod.instIsDomainOfNatNat : IsDomain (ZMod 0)

def ZMod.finEquiv (n : ℕ) [NeZero n] : Fin n ≃+* ZMod n

For non-zero n : ℕ, the ring Fin n is equivalent to ZMod n.

instance ZMod.charZero : CharZero (ZMod 0)

def ZMod.val {n : ℕ} : ZMod n → ℕ

val a is a natural number defined as:

• for a : ZMod 0 it is the absolute value of a
• for a : ZMod n with 0 < n it is the least natural number in the equivalence class

See ZMod.valMinAbs for a variant that takes values in the integers.

theorem ZMod.val_lt {n : ℕ} [NeZero n] (a : ZMod n) : a.val < n

theorem ZMod.val_le {n : ℕ} [NeZero n] (a : ZMod n) : a.val ≤ n

@[simp]

theorem ZMod.val_zero {n : ℕ} : val 0 = 0

@[simp]

theorem ZMod.val_one' : val 1 = 1

@[simp]

theorem ZMod.val_neg' {n : ZMod 0} : (-n).val = n.val

@[simp]

theorem ZMod.val_mul' {m n : ZMod 0} : (m * n).val = m.val * n.val

@[simp]

theorem ZMod.val_natCast (n a : ℕ) : (↑a).val = a % n

theorem ZMod.val_natCast_of_lt {n a : ℕ} (h : a < n) : (↑a).val = a

theorem ZMod.val_ofNat (n a : ℕ) [a.AtLeastTwo] : (OfNat.ofNat a).val = OfNat.ofNat a % n

theorem ZMod.val_ofNat_of_lt {n a : ℕ} [a.AtLeastTwo] (han : a < n) : (OfNat.ofNat a).val = OfNat.ofNat a

theorem ZMod.val_unit' {n : ZMod 0} : IsUnit n ↔ n.val = 1

theorem ZMod.eq_one_of_isUnit_natCast {n : ℕ} (h : IsUnit ↑n) : n = 1

instance ZMod.charP (n : ℕ) : CharP (ZMod n) n

@[simp]

theorem ZMod.addOrderOf_one (n : ℕ) : addOrderOf 1 = n

@[simp]

theorem ZMod.addOrderOf_coe (a : ℕ) {n : ℕ} (n0 : n ≠ 0) : addOrderOf ↑a = n / n.gcd a

This lemma works in the case in which ZMod n is not infinite, i.e. n ≠ 0. The version where a ≠ 0 is addOrderOf_coe'.

@[simp]

theorem ZMod.addOrderOf_coe' {a : ℕ} (n : ℕ) (a0 : a ≠ 0) : addOrderOf ↑a = n / n.gcd a

This lemma works in the case in which a ≠ 0. The version where ZMod n is not infinite, i.e. n ≠ 0, is addOrderOf_coe.

theorem ZMod.ringChar_zmod_n (n : ℕ) : ringChar (ZMod n) = n

We have that ringChar (ZMod n) = n.

theorem ZMod.natCast_self (n : ℕ) : ↑n = 0

@[simp]

theorem ZMod.natCast_self' (n : ℕ) : ↑n + 1 = 0

theorem ZMod.natCast_pow_eq_zero_of_le (p : ℕ) {m n : ℕ} (h : n ≤ m) : ↑p ^ m = 0

def ZMod.cast {R : Type u_1} [AddGroupWithOne R] {n : ℕ} : ZMod n → R

Cast an integer modulo n to another semiring. This function is a morphism if the characteristic of R divides n. See ZMod.castHom for a bundled version.

@[simp]

theorem ZMod.cast_zero {n : ℕ} {R : Type u_1} [AddGroupWithOne R] : cast 0 = 0

theorem ZMod.cast_eq_val {n : ℕ} {R : Type u_1} [AddGroupWithOne R] [NeZero n] (a : ZMod n) : a.cast = ↑a.val

@[simp]

theorem Prod.fst_zmod_cast {n : ℕ} {R : Type u_1} [AddGroupWithOne R] {S : Type u_2} [AddGroupWithOne S] (a : ZMod n) : a.cast.1 = a.cast

@[simp]

theorem Prod.snd_zmod_cast {n : ℕ} {R : Type u_1} [AddGroupWithOne R] {S : Type u_2} [AddGroupWithOne S] (a : ZMod n) : a.cast.2 = a.cast

theorem ZMod.natCast_zmod_val {n : ℕ} [NeZero n] (a : ZMod n) : ↑a.val = a

So-named because the coercion is Nat.cast into ZMod. For Nat.cast into an arbitrary ring, see ZMod.natCast_val.

theorem ZMod.natCast_rightInverse {n : ℕ} [NeZero n] : Function.RightInverse val Nat.cast

theorem ZMod.natCast_zmod_surjective {n : ℕ} [NeZero n] : Function.Surjective Nat.cast

theorem ZMod.intCast_zmod_cast {n : ℕ} (a : ZMod n) : ↑a.cast = a

So-named because the outer coercion is Int.cast into ZMod. For Int.cast into an arbitrary ring, see ZMod.intCast_cast.

theorem ZMod.intCast_rightInverse {n : ℕ} : Function.RightInverse cast Int.cast

theorem ZMod.intCast_surjective {n : ℕ} : Function.Surjective Int.cast

theorem ZMod.forall {n : ℕ} {P : ZMod n → Prop} : (∀ (x : ZMod n), P x) ↔ ∀ (x : ℤ), P ↑x

theorem ZMod.exists {n : ℕ} {P : ZMod n → Prop} : (∃ (x : ZMod n), P x) ↔ ∃ (x : ℤ), P ↑x

theorem ZMod.cast_id (n : ℕ) (i : ZMod n) : i.cast = i

@[simp]

theorem ZMod.cast_id' {n : ℕ} : cast = id

@[simp]

theorem ZMod.natCast_comp_val {n : ℕ} (R : Type u_1) [Ring R] [NeZero n] : Nat.cast ∘ val = cast

The coercions are respectively Nat.cast and ZMod.cast.

@[simp]

theorem ZMod.intCast_comp_cast {n : ℕ} (R : Type u_1) [Ring R] : Int.cast ∘ cast = cast

The coercions are respectively Int.cast, ZMod.cast, and ZMod.cast.

@[simp]

theorem ZMod.natCast_val {n : ℕ} {R : Type u_1} [Ring R] [NeZero n] (i : ZMod n) : ↑i.val = i.cast

@[simp]

theorem ZMod.intCast_cast {n : ℕ} {R : Type u_1} [Ring R] (i : ZMod n) : ↑i.cast = i.cast

theorem ZMod.cast_add_eq_ite {n : ℕ} (a b : ZMod n) : (a + b).cast = if ↑n ≤ a.cast + b.cast then a.cast + b.cast - ↑n else a.cast + b.cast

If the characteristic of R divides n, then cast is a homomorphism.

@[simp]

theorem ZMod.cast_one {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] (h : m ∣ n) : cast 1 = 1

@[simp]

theorem ZMod.cast_add {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] (h : m ∣ n) (a b : ZMod n) : (a + b).cast = a.cast + b.cast

@[simp]

theorem ZMod.cast_mul {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] (h : m ∣ n) (a b : ZMod n) : (a * b).cast = a.cast * b.cast

def ZMod.castHom {n m : ℕ} (h : m ∣ n) (R : Type u_2) [Ring R] [CharP R m] : ZMod n →+* R

The canonical ring homomorphism from ZMod n to a ring of characteristic dividing n.

See also ZMod.lift for a generalized version working in AddGroups.

@[simp]

theorem ZMod.castHom_apply {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] {h : m ∣ n} (i : ZMod n) : (castHom h R) i = i.cast

@[simp]

theorem ZMod.cast_sub {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] (h : m ∣ n) (a b : ZMod n) : (a - b).cast = a.cast - b.cast

@[simp]

theorem ZMod.cast_neg {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] (h : m ∣ n) (a : ZMod n) : (-a).cast = -a.cast

@[simp]

theorem ZMod.cast_pow {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] (h : m ∣ n) (a : ZMod n) (k : ℕ) : (a ^ k).cast = a.cast ^ k

@[simp]

theorem ZMod.cast_natCast {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] (h : m ∣ n) (k : ℕ) : (↑k).cast = ↑k

@[simp]

theorem ZMod.cast_intCast {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] (h : m ∣ n) (k : ℤ) : (↑k).cast = ↑k

theorem ZMod.castHom_surjective {n m : ℕ} (h : m ∣ n) : Function.Surjective ⇑(castHom h (ZMod m))

Some specialised simp lemmas which apply when R has characteristic n.

theorem ZMod.cast_one' {n : ℕ} {R : Type u_1} [Ring R] [CharP R n] : cast 1 = 1

theorem ZMod.cast_add' {n : ℕ} {R : Type u_1} [Ring R] [CharP R n] (a b : ZMod n) : (a + b).cast = a.cast + b.cast

theorem ZMod.cast_mul' {n : ℕ} {R : Type u_1} [Ring R] [CharP R n] (a b : ZMod n) : (a * b).cast = a.cast * b.cast

theorem ZMod.cast_sub' {n : ℕ} {R : Type u_1} [Ring R] [CharP R n] (a b : ZMod n) : (a - b).cast = a.cast - b.cast

theorem ZMod.cast_pow' {n : ℕ} {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (k : ℕ) : (a ^ k).cast = a.cast ^ k

theorem ZMod.cast_natCast' {n : ℕ} {R : Type u_1} [Ring R] [CharP R n] (k : ℕ) : (↑k).cast = ↑k

theorem ZMod.cast_intCast' {n : ℕ} {R : Type u_1} [Ring R] [CharP R n] (k : ℤ) : (↑k).cast = ↑k

theorem ZMod.castHom_injective {n : ℕ} (R : Type u_1) [Ring R] [CharP R n] : Function.Injective ⇑(castHom ⋯ R)

theorem ZMod.castHom_bijective {n : ℕ} (R : Type u_1) [Ring R] [CharP R n] [Fintype R] (h : Fintype.card R = n) : Function.Bijective ⇑(castHom ⋯ R)

noncomputable def ZMod.ringEquiv {n : ℕ} (R : Type u_1) [Ring R] [CharP R n] [Fintype R] (h : Fintype.card R = n) : ZMod n ≃+* R

The unique ring isomorphism between ZMod n and a ring R of characteristic n and cardinality n.

noncomputable def ZMod.ringEquivOfPrime (R : Type u_1) [Ring R] [Fintype R] {p : ℕ} (hp : Nat.Prime p) (hR : Fintype.card R = p) : ZMod p ≃+* R

The unique ring isomorphism between ZMod p and a ring R of cardinality a prime p.

If you need any property of this isomorphism, first of all use ringEquivOfPrime_eq_ringEquiv below (after have : CharP R p := ...) and deduce it by the results about ZMod.ringEquiv.

@[simp]

theorem ZMod.ringEquivOfPrime_eq_ringEquiv (R : Type u_1) [Ring R] [Fintype R] {p : ℕ} [CharP R p] (hp : Nat.Prime p) (hR : Fintype.card R = p) : ringEquivOfPrime R hp hR = ringEquiv R hR

def ZMod.ringEquivCongr {m n : ℕ} (h : m = n) : ZMod m ≃+* ZMod n

The identity between ZMod m and ZMod n when m = n, as a ring isomorphism.

@[simp]

theorem ZMod.ringEquivCongr_refl (a : ℕ) : ringEquivCongr ⋯ = RingEquiv.refl (ZMod a)

theorem ZMod.ringEquivCongr_refl_apply {a : ℕ} (x : ZMod a) : (ringEquivCongr ⋯) x = x

theorem ZMod.ringEquivCongr_symm {a b : ℕ} (hab : a = b) : (ringEquivCongr hab).symm = ringEquivCongr ⋯

theorem ZMod.ringEquivCongr_trans {a b c : ℕ} (hab : a = b) (hbc : b = c) : (ringEquivCongr hab).trans (ringEquivCongr hbc) = ringEquivCongr ⋯

theorem ZMod.ringEquivCongr_ringEquivCongr_apply {a b c : ℕ} (hab : a = b) (hbc : b = c) (x : ZMod a) : (ringEquivCongr hbc) ((ringEquivCongr hab) x) = (ringEquivCongr ⋯) x

theorem ZMod.ringEquivCongr_val {a b : ℕ} (h : a = b) (x : ZMod a) : ((ringEquivCongr h) x).val = x.val

theorem ZMod.ringEquivCongr_intCast {a b : ℕ} (h : a = b) (z : ℤ) : (ringEquivCongr h) ↑z = ↑z

@[simp]

theorem ZMod.val_eq_zero {n : ℕ} (a : ZMod n) : a.val = 0 ↔ a = 0

theorem ZMod.intCast_eq_intCast_iff (a b : ℤ) (c : ℕ) : ↑a = ↑b ↔ a ≡ b [ZMOD ↑c]

theorem ZMod.intCast_eq_intCast_iff' (a b : ℤ) (c : ℕ) : ↑a = ↑b ↔ a % ↑c = b % ↑c

theorem ZMod.val_intCast {n : ℕ} (a : ℤ) [NeZero n] : ↑(↑a).val = a % ↑n

theorem ZMod.natCast_eq_natCast_iff (a b c : ℕ) : ↑a = ↑b ↔ a ≡ b [MOD c]

theorem ZMod.natCast_eq_natCast_iff' (a b c : ℕ) : ↑a = ↑b ↔ a % c = b % c

theorem ZMod.intCast_zmod_eq_zero_iff_dvd (a : ℤ) (b : ℕ) : ↑a = 0 ↔ ↑b ∣ a

theorem ZMod.intCast_eq_intCast_iff_dvd_sub (a b : ℤ) (c : ℕ) : ↑a = ↑b ↔ ↑c ∣ b - a

theorem ZMod.natCast_eq_zero_iff (a b : ℕ) : ↑a = 0 ↔ b ∣ a

theorem ZMod.coe_intCast {n : ℕ} (a : ℤ) : (↑a).cast = a % ↑n

theorem ZMod.intCast_cast_add {n : ℕ} (x y : ZMod n) : (x + y).cast = (x.cast + y.cast) % ↑n

theorem ZMod.intCast_cast_mul {n : ℕ} (x y : ZMod n) : (x * y).cast = x.cast * y.cast % ↑n

theorem ZMod.intCast_cast_sub {n : ℕ} (x y : ZMod n) : (x - y).cast = (x.cast - y.cast) % ↑n

theorem ZMod.intCast_cast_neg {n : ℕ} (x : ZMod n) : (-x).cast = -x.cast % ↑n

@[simp]

theorem ZMod.val_neg_one (n : ℕ) : (-1).val = n

theorem ZMod.cast_neg_one {R : Type u_1} [Ring R] (n : ℕ) : (-1).cast = ↑n - 1

-1 : ZMod n lifts to n - 1 : R. This avoids the characteristic assumption in cast_neg.

theorem ZMod.cast_sub_one {R : Type u_1} [Ring R] {n : ℕ} (k : ZMod n) : (k - 1).cast = (if k = 0 then ↑n else k.cast) - 1

theorem ZMod.natCast_eq_iff (p n : ℕ) (z : ZMod p) [NeZero p] : ↑n = z ↔ ∃ (k : ℕ), n = z.val + p * k

theorem ZMod.intCast_eq_iff (p : ℕ) (n : ℤ) (z : ZMod p) [NeZero p] : ↑n = z ↔ ∃ (k : ℤ), n = ↑z.val + ↑p * k

@[simp]

theorem ZMod.intCast_mod (a : ℤ) (b : ℕ) : ↑(a % ↑b) = ↑a

theorem ZMod.ker_intCastAddHom (n : ℕ) : (Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples ↑n

theorem ZMod.cast_injective_of_le {m n : ℕ} [nzm : NeZero m] (h : m ≤ n) : Function.Injective cast

theorem ZMod.cast_zmod_eq_zero_iff_of_le {m n : ℕ} [NeZero m] (h : m ≤ n) (a : ZMod m) : a.cast = 0 ↔ a = 0

@[simp]

theorem ZMod.natCast_toNat (p : ℕ) {z : ℤ} (_h : 0 ≤ z) : ↑z.toNat = ↑z

theorem ZMod.val_injective (n : ℕ) [NeZero n] : Function.Injective val

theorem ZMod.val_one_eq_one_mod (n : ℕ) : val 1 = 1 % n

theorem ZMod.val_two_eq_two_mod (n : ℕ) : val 2 = 2 % n

theorem ZMod.val_one (n : ℕ) [Fact (1 < n)] : val 1 = 1

theorem ZMod.val_one'' {n : ℕ} : n ≠ 1 → val 1 = 1

theorem ZMod.val_add {n : ℕ} [NeZero n] (a b : ZMod n) : (a + b).val = (a.val + b.val) % n

theorem ZMod.val_add_of_lt {n : ℕ} {a b : ZMod n} (h : a.val + b.val < n) : (a + b).val = a.val + b.val

theorem ZMod.val_add_val_of_le {n : ℕ} [NeZero n] {a b : ZMod n} (h : n ≤ a.val + b.val) : a.val + b.val = (a + b).val + n

theorem ZMod.val_add_of_le {n : ℕ} [NeZero n] {a b : ZMod n} (h : n ≤ a.val + b.val) : (a + b).val = a.val + b.val - n

theorem ZMod.val_add_le {n : ℕ} (a b : ZMod n) : (a + b).val ≤ a.val + b.val

theorem ZMod.val_mul {n : ℕ} (a b : ZMod n) : (a * b).val = a.val * b.val % n

theorem ZMod.val_mul_le {n : ℕ} (a b : ZMod n) : (a * b).val ≤ a.val * b.val

theorem ZMod.val_mul_of_lt {n : ℕ} {a b : ZMod n} (h : a.val * b.val < n) : (a * b).val = a.val * b.val

theorem ZMod.val_mul_iff_lt {n : ℕ} [NeZero n] (a b : ZMod n) : (a * b).val = a.val * b.val ↔ a.val * b.val < n

instance ZMod.nontrivial (n : ℕ) [Fact (1 < n)] : Nontrivial (ZMod n)

instance ZMod.nontrivial' : Nontrivial (ZMod 0)

theorem ZMod.one_eq_zero_iff {n : ℕ} : 1 = 0 ↔ n = 1

def ZMod.inv (n : ℕ) : ZMod n → ZMod n

The inversion on ZMod n. It is setup in such a way that a * a⁻¹ is equal to gcd a.val n. In particular, if a is coprime to n, and hence a unit, a * a⁻¹ = 1.

instance ZMod.instInv (n : ℕ) : Inv (ZMod n)

theorem ZMod.inv_zero (n : ℕ) : 0⁻¹ = 0

theorem ZMod.mul_inv_eq_gcd {n : ℕ} (a : ZMod n) : a * a⁻¹ = ↑(a.val.gcd n)

@[simp]

theorem ZMod.inv_one (n : ℕ) : 1⁻¹ = 1

@[simp]

theorem ZMod.natCast_mod (a n : ℕ) : ↑(a % n) = ↑a

theorem ZMod.intCast_eq_zero_iff_even {n : ℤ} : ↑n = 0 ↔ Even n

theorem Even.intCast_zmod_two {n : ℤ} : Even n → ↑n = 0

Alias of the reverse direction of ZMod.intCast_eq_zero_iff_even.

theorem ZMod.natCast_eq_zero_iff_even {n : ℕ} : ↑n = 0 ↔ Even n

@[deprecated ZMod.natCast_eq_zero_iff_even (since := "2025-08-25")]

theorem ZMod.eq_zero_iff_even {n : ℕ} : ↑n = 0 ↔ Even n

Alias of ZMod.natCast_eq_zero_iff_even.

theorem Even.natCast_zmod_two {n : ℕ} : Even n → ↑n = 0

Alias of the reverse direction of ZMod.natCast_eq_zero_iff_even.

theorem ZMod.intCast_eq_one_iff_odd {n : ℤ} : ↑n = 1 ↔ Odd n

theorem Odd.intCast_zmod_two {n : ℤ} : Odd n → ↑n = 1

Alias of the reverse direction of ZMod.intCast_eq_one_iff_odd.

theorem ZMod.natCast_eq_one_iff_odd {n : ℕ} : ↑n = 1 ↔ Odd n

@[deprecated ZMod.natCast_eq_one_iff_odd (since := "2025-08-25")]

theorem ZMod.eq_one_iff_odd {n : ℕ} : ↑n = 1 ↔ Odd n

Alias of ZMod.natCast_eq_one_iff_odd.

theorem Odd.natCast_zmod_two {n : ℕ} : Odd n → ↑n = 1

Alias of the reverse direction of ZMod.natCast_eq_one_iff_odd.

theorem ZMod.natCast_ne_zero_iff_odd {n : ℕ} : ↑n ≠ 0 ↔ Odd n

@[deprecated ZMod.natCast_ne_zero_iff_odd (since := "2025-08-25")]

theorem ZMod.ne_zero_iff_odd {n : ℕ} : ↑n ≠ 0 ↔ Odd n

Alias of ZMod.natCast_ne_zero_iff_odd.

theorem ZMod.coe_mul_inv_eq_one {n : ℕ} (x : ℕ) (h : x.Coprime n) : ↑x * (↑x)⁻¹ = 1

theorem ZMod.mul_val_inv {m n : ℕ} (hmn : m.Coprime n) : ↑m * ↑(↑m)⁻¹.val = 1

theorem ZMod.val_inv_mul {m n : ℕ} (hmn : m.Coprime n) : ↑(↑m)⁻¹.val * ↑m = 1

def ZMod.unitOfCoprime {n : ℕ} (x : ℕ) (h : x.Coprime n) : (ZMod n)ˣ

unitOfCoprime makes an element of (ZMod n)ˣ given a natural number x and a proof that x is coprime to n

@[simp]

theorem ZMod.coe_unitOfCoprime {n : ℕ} (x : ℕ) (h : x.Coprime n) : ↑(unitOfCoprime x h) = ↑x

theorem ZMod.val_coe_unit_coprime {n : ℕ} (u : (ZMod n)ˣ) : (↑u).val.Coprime n

theorem ZMod.isUnit_iff_coprime (m n : ℕ) : IsUnit ↑m ↔ m.Coprime n

@[simp]

theorem ZMod.coprime_mod_iff_coprime (m n : ℕ) : (m % n).Coprime n ↔ m.Coprime n

theorem ZMod.isUnit_prime_iff_not_dvd {n p : ℕ} (hp : Nat.Prime p) : IsUnit ↑p ↔ ¬p ∣ n

theorem ZMod.isUnit_prime_of_not_dvd {n p : ℕ} (hp : Nat.Prime p) (h : ¬p ∣ n) : IsUnit ↑p

@[simp]

theorem ZMod.inv_coe_unit {n : ℕ} (u : (ZMod n)ˣ) : (↑u)⁻¹ = ↑u⁻¹

theorem ZMod.mul_inv_of_unit {n : ℕ} (a : ZMod n) (h : IsUnit a) : a * a⁻¹ = 1

theorem ZMod.inv_mul_of_unit {n : ℕ} (a : ZMod n) (h : IsUnit a) : a⁻¹ * a = 1

theorem ZMod.inv_eq_of_mul_eq_one (n : ℕ) (a b : ZMod n) (h : a * b = 1) : a⁻¹ = b

@[simp]

theorem ZMod.inv_neg_one (n : ℕ) : (-1)⁻¹ = -1

theorem ZMod.inv_mul_eq_one_of_isUnit {n : ℕ} {a : ZMod n} (ha : IsUnit a) (b : ZMod n) : a⁻¹ * b = 1 ↔ a = b

def ZMod.unitsEquivCoprime {n : ℕ} [NeZero n] : (ZMod n)ˣ ≃ { x : ZMod n // x.val.Coprime n }

Equivalence between the units of ZMod n and the subtype of terms x : ZMod n for which x.val is coprime to n

def ZMod.chineseRemainder {m n : ℕ} (h : m.Coprime n) : ZMod (m * n) ≃+* ZMod m × ZMod n

The Chinese remainder theorem. For a pair of coprime natural numbers, m and n, the rings ZMod (m * n) and ZMod m × ZMod n are isomorphic.

See Ideal.quotientInfRingEquivPiQuotient for the Chinese remainder theorem for ideals in any ring.

theorem ZMod.subsingleton_iff {n : ℕ} : Subsingleton (ZMod n) ↔ n = 1

theorem ZMod.nontrivial_iff {n : ℕ} : Nontrivial (ZMod n) ↔ n ≠ 1

instance ZMod.instSubsingletonUnits : Subsingleton (ZMod 2)ˣ

@[simp]

theorem ZMod.add_self_eq_zero_iff_eq_zero {n : ℕ} (hn : Odd n) {a : ZMod n} : a + a = 0 ↔ a = 0

theorem ZMod.ne_neg_self {n : ℕ} (hn : Odd n) {a : ZMod n} (ha : a ≠ 0) : a ≠ -a

theorem ZMod.neg_one_ne_one {n : ℕ} [Fact (2 < n)] : -1 ≠ 1

@[simp]

theorem ZMod.neg_eq_self_mod_two (a : ZMod 2) : -a = a

@[simp]

theorem ZMod.intCast_abs_mod_two (a : ℤ) : ↑|a| = ↑a

theorem ZMod.natAbs_mod_two (a : ℤ) : ↑a.natAbs = ↑a

theorem ZMod.val_ne_zero {n : ℕ} (a : ZMod n) : a.val ≠ 0 ↔ a ≠ 0

@[simp]

theorem ZMod.val_pos {n : ℕ} {a : ZMod n} : 0 < a.val ↔ a ≠ 0

theorem ZMod.val_eq_one {n : ℕ} : 1 < n → ∀ (a : ZMod n), a.val = 1 ↔ a = 1

theorem ZMod.neg_eq_self_iff {n : ℕ} (a : ZMod n) : -a = a ↔ a = 0 ∨ 2 * a.val = n

theorem ZMod.val_cast_of_lt {n a : ℕ} (h : a < n) : (↑a).val = a

theorem ZMod.val_cast_zmod_lt {m : ℕ} [NeZero m] (n : ℕ) [NeZero n] (a : ZMod m) : a.cast.val < m

theorem ZMod.neg_val' {n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = (n - a.val) % n

theorem ZMod.neg_val {n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = if a = 0 then 0 else n - a.val

theorem ZMod.val_neg_of_ne_zero {n : ℕ} [nz : NeZero n] (a : ZMod n) [na : NeZero a] : (-a).val = n - a.val

theorem ZMod.val_sub {n : ℕ} [NeZero n] {a b : ZMod n} (h : b.val ≤ a.val) : (a - b).val = a.val - b.val

theorem ZMod.val_cast_eq_val_of_lt {m n : ℕ} [nzm : NeZero m] {a : ZMod m} (h : a.val < n) : a.cast.val = a.val

theorem ZMod.cast_cast_zmod_of_le {m n : ℕ} [hm : NeZero m] (h : m ≤ n) (a : ZMod m) : a.cast.cast = a

theorem ZMod.val_pow {m n : ℕ} {a : ZMod n} [ilt : Fact (1 < n)] (h : a.val ^ m < n) : (a ^ m).val = a.val ^ m

theorem ZMod.val_pow_le {m n : ℕ} [Fact (1 < n)] {a : ZMod n} : (a ^ m).val ≤ a.val ^ m

theorem ZMod.natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : ↑x = ↑y) (hl : x.natAbs ≤ n / 2) : x.natAbs ≤ y.natAbs

theorem RingHom.ext_zmod {n : ℕ} {R : Type u_1} [NonAssocSemiring R] (f g : ZMod n →+* R) : f = g

instance ZMod.subsingleton_ringHom {n : ℕ} {R : Type u_1} [Semiring R] : Subsingleton (ZMod n →+* R)

instance ZMod.subsingleton_ringEquiv {n : ℕ} {R : Type u_1} [Semiring R] : Subsingleton (ZMod n ≃+* R)

@[simp]

theorem ZMod.ringHom_map_cast {n : ℕ} {R : Type u_1} [NonAssocRing R] (f : R →+* ZMod n) (k : ZMod n) : f k.cast = k

theorem ZMod.ringHom_rightInverse {n : ℕ} {R : Type u_1} [NonAssocRing R] (f : R →+* ZMod n) : Function.RightInverse cast ⇑f

Any ring homomorphism into ZMod n has a right inverse.

theorem ZMod.ringHom_surjective {n : ℕ} {R : Type u_1} [NonAssocRing R] (f : R →+* ZMod n) : Function.Surjective ⇑f

Any ring homomorphism into ZMod n is surjective.

@[simp]

theorem ZMod.castHom_self {n : ℕ} : castHom ⋯ (ZMod n) = RingHom.id (ZMod n)

@[simp]

theorem ZMod.castHom_comp {n m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) : (castHom hm (ZMod n)).comp (castHom hd (ZMod m)) = castHom ⋯ (ZMod n)

def ZMod.lift (n : ℕ) {A : Type u_2} [AddGroup A] : { f : ℤ →+ A // f ↑n = 0 } ≃ (ZMod n →+ A)

The map from ZMod n induced by f : ℤ →+ A that maps n to 0.

@[simp]

theorem ZMod.lift_coe (n : ℕ) {A : Type u_2} [AddGroup A] (f : { f : ℤ →+ A // f ↑n = 0 }) (x : ℤ) : ((lift n) f) ↑x = ↑f x

theorem ZMod.lift_castAddHom (n : ℕ) {A : Type u_2} [AddGroup A] (f : { f : ℤ →+ A // f ↑n = 0 }) (x : ℤ) : ((lift n) f) ((Int.castAddHom (ZMod n)) x) = ↑f x

@[simp]

theorem ZMod.lift_comp_coe (n : ℕ) {A : Type u_2} [AddGroup A] (f : { f : ℤ →+ A // f ↑n = 0 }) : ⇑((lift n) f) ∘ Int.cast = ⇑↑f

@[simp]

theorem ZMod.lift_comp_castAddHom (n : ℕ) {A : Type u_2} [AddGroup A] (f : { f : ℤ →+ A // f ↑n = 0 }) : ((lift n) f).comp (Int.castAddHom (ZMod n)) = ↑f

theorem ZMod.lift_injective (n : ℕ) {A : Type u_2} [AddGroup A] {f : { f : ℤ →+ A // f ↑n = 0 }} : Function.Injective ⇑((lift n) f) ↔ ∀ (m : ℤ), ↑f m = 0 → ↑m = 0

Groups of bounded torsion

For G a group and n a natural number, G having torsion dividing n (∀ x : G, n • x = 0) can be derived from Module R G where R has characteristic dividing n.

It is however painful to have the API for such groups G stated in this generality, as R does not appear anywhere in the lemmas' return type. Instead of writing the API in terms of a general R, we therefore specialise to the canonical ring of order n, namely ZMod n.

This spelling Module (ZMod n) G has the extra advantage of providing the canonical action by ZMod n. It is however Type-valued, so we might want to acquire a Prop-valued version in the future.

theorem zmod_smul_mem {n : ℕ} {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] {K : S} [Module (ZMod n) G] {x : G} (hx : x ∈ K) (a : ZMod n) : a • x ∈ K

theorem smulMemClass {n : ℕ} {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] [Module (ZMod n) G] : SMulMemClass S (ZMod n) G

This cannot be made an instance because of the [Module (ZMod n) G] argument and the fact that n only appears in the second argument of SMulMemClass, which is an OutParam.

instance AddSubgroupClass.instZModSMul {n : ℕ} {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] {K : S} [Module (ZMod n) G] : SMul (ZMod n) ↥K

@[simp]

theorem AddSubgroupClass.coe_zmod_smul {n : ℕ} {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] {K : S} [Module (ZMod n) G] (a : ZMod n) (x : ↥K) : ↑(a • x) = a • ↑x

instance AddSubgroupClass.instZModModule {n : ℕ} {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] {K : S} [Module (ZMod n) G] : Module (ZMod n) ↥K

theorem ZModModule.char_nsmul_eq_zero (n : ℕ) {G : Type u_2} [AddCommGroup G] [Module (ZMod n) G] (x : G) : n • x = 0

theorem ZModModule.char_ne_one (n : ℕ) (G : Type u_2) [AddCommGroup G] [Module (ZMod n) G] [Nontrivial G] : n ≠ 1

theorem ZModModule.two_le_char (n : ℕ) (G : Type u_2) [AddCommGroup G] [Module (ZMod n) G] [NeZero n] [Nontrivial G] : 2 ≤ n

theorem ZModModule.periodicPts_add_left (n : ℕ) {G : Type u_2} [AddCommGroup G] [Module (ZMod n) G] [NeZero n] (x : G) : (Function.periodicPts fun (x_1 : G) => x + x_1) = Set.univ

theorem ZModModule.add_self {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] (x : G) : x + x = 0

theorem ZModModule.neg_eq_self {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] (x : G) : -x = x

theorem ZModModule.sub_eq_add {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] (x y : G) : x - y = x + y

theorem ZModModule.add_add_add_cancel {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] (x y z : G) : x + y + (y + z) = x + z

@[simp]

theorem pow_zmod_val_inv_pow {α : Type u_1} [Group α] {n : ℕ} (hn : (Nat.card α).gcd n = 1) (a : α) : (a ^ (↑n)⁻¹.val) ^ n = a

@[simp]

theorem nsmul_zmod_val_inv_nsmul {α : Type u_1} [AddGroup α] {n : ℕ} (hn : (Nat.card α).gcd n = 1) (a : α) : n • (↑n)⁻¹.val • a = a

@[simp]

theorem pow_pow_zmod_val_inv {α : Type u_1} [Group α] {n : ℕ} (hn : (Nat.card α).gcd n = 1) (a : α) : (a ^ n) ^ (↑n)⁻¹.val = a

@[simp]

theorem zmod_val_inv_nsmul_nsmul {α : Type u_1} [AddGroup α] {n : ℕ} (hn : (Nat.card α).gcd n = 1) (a : α) : (↑n)⁻¹.val • n • a = a

theorem Nat.range_mul_add (m k : ℕ) : (Set.range fun (n : ℕ) => m * n + k) = {n : ℕ | ↑n = ↑k ∧ k ≤ n}

The range of (m * · + k) on natural numbers is the set of elements ≥ k in the residue class of k mod m.

def Nat.residueClassesEquiv (N : ℕ) [NeZero N] : ℕ ≃ ZMod N × ℕ

Equivalence between ℕ and ZMod N × ℕ, sending n to (n mod N, n / N).

instance ZMod.instSubsingletonModule (n : ℕ) (M : Type u_1) [AddCommMonoid M] : Subsingleton (Module (ZMod n) M)