# 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`

source
instance ZMod.instIsDomainOfNatNat :
IsDomain (ZMod 0)
source
def ZMod.finEquiv (n : ℕ) [NeZero n] :
Fin n ≃+* ZMod n

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

Equations

- ZMod.finEquiv 0 = ⋯.elim
- ZMod.finEquiv n.succ = RingEquiv.refl (Fin (n + 1))

Instances For

source
instance ZMod.charZero :
CharZero (ZMod 0)
source
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.

Equations

- ZMod.val = Int.natAbs
- ZMod.val = Fin.val

Instances For

source
theorem ZMod.val_lt {n : ℕ} [NeZero n] (a : ZMod n) :
a.val < n
source
theorem ZMod.val_le {n : ℕ} [NeZero n] (a : ZMod n) :
a.val ≤ n
source
@[simp]
theorem ZMod.val_zero {n : ℕ} :
val 0 = 0
source
@[simp]
theorem ZMod.val_one' :
val 1 = 1
source
@[simp]
theorem ZMod.val_neg' {n : ZMod 0} :
(-n).val = n.val
source
@[simp]
theorem ZMod.val_mul' {m n : ZMod 0} :
(m * n).val = m.val * n.val
source
@[simp]
theorem ZMod.val_natCast (n a : ℕ) :
(↑a).val = a % n
source
theorem ZMod.val_natCast_of_lt {n a : ℕ} (h : a < n) :
(↑a).val = a
source
theorem ZMod.val_ofNat (n a : ℕ) [a.AtLeastTwo] :
(OfNat.ofNat a).val = OfNat.ofNat a % n
source
theorem ZMod.val_ofNat_of_lt {n a : ℕ} [a.AtLeastTwo] (han : a < n) :
(OfNat.ofNat a).val = OfNat.ofNat a
source
theorem ZMod.val_unit' {n : ZMod 0} :
IsUnit n ↔ n.val = 1
source
theorem ZMod.eq_one_of_isUnit_natCast {n : ℕ} (h : IsUnit ↑n) :
n = 1
source
instance ZMod.charP (n : ℕ) :
CharP (ZMod n) n
source
@[simp]
theorem ZMod.addOrderOf_one (n : ℕ) :
addOrderOf 1 = n
source
@[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'`.

source
@[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`.

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

We have that `ringChar (ZMod n) = n`.

source
theorem ZMod.natCast_self (n : ℕ) :
↑n = 0
source
@[simp]
theorem ZMod.natCast_self' (n : ℕ) :
↑n + 1 = 0
source
theorem ZMod.natCast_pow_eq_zero_of_le (p : ℕ) {m n : ℕ} (h : n ≤ m) :
↑p ^ m = 0
source
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.

Equations

- ZMod.cast = Int.cast
- ZMod.cast = fun (i : ZMod (n + 1)) => ↑i.val

Instances For

source
@[simp]
theorem ZMod.cast_zero {n : ℕ} {R : Type u_1} [AddGroupWithOne R] :
cast 0 = 0
source
theorem ZMod.cast_eq_val {n : ℕ} {R : Type u_1} [AddGroupWithOne R] [NeZero n] (a : ZMod n) :
a.cast = ↑a.val
source
@[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
source
@[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
source
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`.

source
theorem ZMod.natCast_rightInverse {n : ℕ} [NeZero n] :
Function.RightInverse val Nat.cast
source
theorem ZMod.natCast_zmod_surjective {n : ℕ} [NeZero n] :
Function.Surjective Nat.cast
source
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`.

source
theorem ZMod.intCast_rightInverse {n : ℕ} :
Function.RightInverse cast Int.cast
source
theorem ZMod.intCast_surjective {n : ℕ} :
Function.Surjective Int.cast
source
theorem ZMod.forall {n : ℕ} {P : ZMod n → Prop} :
(∀ (x : ZMod n), P x) ↔ ∀ (x : ℤ), P ↑x
source
theorem ZMod.exists {n : ℕ} {P : ZMod n → Prop} :
(∃ (x : ZMod n), P x) ↔ ∃ (x : ℤ), P ↑x
source
theorem ZMod.cast_id (n : ℕ) (i : ZMod n) :
i.cast = i
source
@[simp]
theorem ZMod.cast_id' {n : ℕ} :
cast = id
source
@[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`.

source
@[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`.

source
@[simp]
theorem ZMod.natCast_val {n : ℕ} {R : Type u_1} [Ring R] [NeZero n] (i : ZMod n) :
↑i.val = i.cast
source
@[simp]
theorem ZMod.intCast_cast {n : ℕ} {R : Type u_1} [Ring R] (i : ZMod n) :
↑i.cast = i.cast
source
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.

source
@[simp]
theorem ZMod.cast_one {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] (h : m ∣ n) :
cast 1 = 1
source
@[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
source
@[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
source
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 `AddGroup`s.

Equations

- ZMod.castHom h R = { toFun := ZMod.cast, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[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
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem ZMod.cast_natCast {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] (h : m ∣ n) (k : ℕ) :
(↑k).cast = ↑k
source
@[simp]
theorem ZMod.cast_intCast {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] (h : m ∣ n) (k : ℤ) :
(↑k).cast = ↑k
source
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`.

source
theorem ZMod.cast_one' {n : ℕ} {R : Type u_1} [Ring R] [CharP R n] :
cast 1 = 1
source
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
source
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
source
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
source
theorem ZMod.cast_pow' {n : ℕ} {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (k : ℕ) :
(a ^ k).cast = a.cast ^ k
source
theorem ZMod.cast_natCast' {n : ℕ} {R : Type u_1} [Ring R] [CharP R n] (k : ℕ) :
(↑k).cast = ↑k
source
theorem ZMod.cast_intCast' {n : ℕ} {R : Type u_1} [Ring R] [CharP R n] (k : ℤ) :
(↑k).cast = ↑k
source
theorem ZMod.castHom_injective {n : ℕ} (R : Type u_1) [Ring R] [CharP R n] :
Function.Injective ⇑(castHom ⋯ R)
source
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)
source
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`.

Equations

- ZMod.ringEquiv R h = RingEquiv.ofBijective (ZMod.castHom ⋯ R) ⋯

Instances For

source
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`.

Equations

- ZMod.ringEquivOfPrime R hp hR = ZMod.ringEquiv R hR

Instances For

source
@[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
source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ZMod.ringEquivCongr_refl (a : ℕ) :
ringEquivCongr ⋯ = RingEquiv.refl (ZMod a)
source
theorem ZMod.ringEquivCongr_refl_apply {a : ℕ} (x : ZMod a) :
(ringEquivCongr ⋯) x = x
source
theorem ZMod.ringEquivCongr_symm {a b : ℕ} (hab : a = b) :
(ringEquivCongr hab).symm = ringEquivCongr ⋯
source
theorem ZMod.ringEquivCongr_trans {a b c : ℕ} (hab : a = b) (hbc : b = c) :
(ringEquivCongr hab).trans (ringEquivCongr hbc) = ringEquivCongr ⋯
source
theorem ZMod.ringEquivCongr_ringEquivCongr_apply {a b c : ℕ} (hab : a = b) (hbc : b = c) (x : ZMod a) :
(ringEquivCongr hbc) ((ringEquivCongr hab) x) = (ringEquivCongr ⋯) x
source
theorem ZMod.ringEquivCongr_val {a b : ℕ} (h : a = b) (x : ZMod a) :
((ringEquivCongr h) x).val = x.val
source
theorem ZMod.ringEquivCongr_intCast {a b : ℕ} (h : a = b) (z : ℤ) :
(ringEquivCongr h) ↑z = ↑z
source
@[simp]
theorem ZMod.val_eq_zero {n : ℕ} (a : ZMod n) :
a.val = 0 ↔ a = 0
source
theorem ZMod.intCast_eq_intCast_iff (a b : ℤ) (c : ℕ) :
↑a = ↑b ↔ a ≡ b [ZMOD ↑c]
source
theorem ZMod.intCast_eq_intCast_iff' (a b : ℤ) (c : ℕ) :
↑a = ↑b ↔ a % ↑c = b % ↑c
source
theorem ZMod.val_intCast {n : ℕ} (a : ℤ) [NeZero n] :
↑(↑a).val = a % ↑n
source
theorem ZMod.natCast_eq_natCast_iff (a b c : ℕ) :
↑a = ↑b ↔ a ≡ b [MOD c]
source
theorem ZMod.natCast_eq_natCast_iff' (a b c : ℕ) :
↑a = ↑b ↔ a % c = b % c
source
theorem ZMod.intCast_zmod_eq_zero_iff_dvd (a : ℤ) (b : ℕ) :
↑a = 0 ↔ ↑b ∣ a
source
theorem ZMod.intCast_eq_intCast_iff_dvd_sub (a b : ℤ) (c : ℕ) :
↑a = ↑b ↔ ↑c ∣ b - a
source
theorem ZMod.natCast_eq_zero_iff (a b : ℕ) :
↑a = 0 ↔ b ∣ a
source
@[deprecated ZMod.natCast_eq_zero_iff (since := "2025-06-30")]
theorem ZMod.natCast_zmod_eq_zero_iff_dvd (a b : ℕ) :
↑a = 0 ↔ b ∣ a

Alias of `ZMod.natCast_eq_zero_iff`.

source
theorem ZMod.coe_intCast {n : ℕ} (a : ℤ) :
(↑a).cast = a % ↑n
source
theorem ZMod.intCast_cast_add {n : ℕ} (x y : ZMod n) :
(x + y).cast = (x.cast + y.cast) % ↑n
source
theorem ZMod.intCast_cast_mul {n : ℕ} (x y : ZMod n) :
(x * y).cast = x.cast * y.cast % ↑n
source
theorem ZMod.intCast_cast_sub {n : ℕ} (x y : ZMod n) :
(x - y).cast = (x.cast - y.cast) % ↑n
source
theorem ZMod.intCast_cast_neg {n : ℕ} (x : ZMod n) :
(-x).cast = -x.cast % ↑n
source
@[simp]
theorem ZMod.val_neg_one (n : ℕ) :
(-1).val = n
source
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`.

source
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
source
theorem ZMod.natCast_eq_iff (p n : ℕ) (z : ZMod p) [NeZero p] :
↑n = z ↔ ∃ (k : ℕ), n = z.val + p * k
source
theorem ZMod.intCast_eq_iff (p : ℕ) (n : ℤ) (z : ZMod p) [NeZero p] :
↑n = z ↔ ∃ (k : ℤ), n = ↑z.val + ↑p * k
source
@[simp]
theorem ZMod.intCast_mod (a : ℤ) (b : ℕ) :
↑(a % ↑b) = ↑a
source
theorem ZMod.ker_intCastAddHom (n : ℕ) :
(Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples ↑n
source
theorem ZMod.cast_injective_of_le {m n : ℕ} [nzm : NeZero m] (h : m ≤ n) :
Function.Injective cast
source
theorem ZMod.cast_zmod_eq_zero_iff_of_le {m n : ℕ} [NeZero m] (h : m ≤ n) (a : ZMod m) :
a.cast = 0 ↔ a = 0
source
@[simp]
theorem ZMod.natCast_toNat (p : ℕ) {z : ℤ} (_h : 0 ≤ z) :
↑z.toNat = ↑z
source
theorem ZMod.val_injective (n : ℕ) [NeZero n] :
Function.Injective val
source
theorem ZMod.val_one_eq_one_mod (n : ℕ) :
val 1 = 1 % n
source
theorem ZMod.val_two_eq_two_mod (n : ℕ) :
val 2 = 2 % n
source
theorem ZMod.val_one (n : ℕ) [Fact (1 < n)] :
val 1 = 1
source
theorem ZMod.val_one'' {n : ℕ} :
n ≠ 1 → val 1 = 1
source
theorem ZMod.val_add {n : ℕ} [NeZero n] (a b : ZMod n) :
(a + b).val = (a.val + b.val) % n
source
theorem ZMod.val_add_of_lt {n : ℕ} {a b : ZMod n} (h : a.val + b.val < n) :
(a + b).val = a.val + b.val
source
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
source
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
source
theorem ZMod.val_add_le {n : ℕ} (a b : ZMod n) :
(a + b).val ≤ a.val + b.val
source
theorem ZMod.val_mul {n : ℕ} (a b : ZMod n) :
(a * b).val = a.val * b.val % n
source
theorem ZMod.val_mul_le {n : ℕ} (a b : ZMod n) :
(a * b).val ≤ a.val * b.val
source
theorem ZMod.val_mul_of_lt {n : ℕ} {a b : ZMod n} (h : a.val * b.val < n) :
(a * b).val = a.val * b.val
source
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
source
instance ZMod.nontrivial (n : ℕ) [Fact (1 < n)] :
Nontrivial (ZMod n)
source
instance ZMod.nontrivial' :
Nontrivial (ZMod 0)
source
theorem ZMod.one_eq_zero_iff {n : ℕ} :
1 = 0 ↔ n = 1
source
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`.

Equations

- ZMod.inv 0 i = Int.sign i
- ZMod.inv n.succ i = ↑(i.val.gcdA (n + 1))

Instances For

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

- ZMod.instInv n = { inv := ZMod.inv n }

source
theorem ZMod.inv_zero (n : ℕ) :
0⁻¹ = 0
source
theorem ZMod.mul_inv_eq_gcd {n : ℕ} (a : ZMod n) :
a * a⁻¹ = ↑(a.val.gcd n)
source
@[simp]
theorem ZMod.inv_one (n : ℕ) :
1⁻¹ = 1
source
@[simp]
theorem ZMod.natCast_mod (a n : ℕ) :
↑(a % n) = ↑a
source
@[deprecated ZMod.natCast_eq_natCast_iff (since := "2025-08-12")]
theorem ZMod.eq_iff_modEq_nat (n : ℕ) {a b : ℕ} :
↑a = ↑b ↔ a ≡ b [MOD n]
source
theorem ZMod.intCast_eq_zero_iff_even {n : ℤ} :
↑n = 0 ↔ Even n
source
theorem Even.intCast_zmod_two {n : ℤ} :
Even n → ↑n = 0

Alias of the reverse direction of `ZMod.intCast_eq_zero_iff_even`.

source
theorem ZMod.natCast_eq_zero_iff_even {n : ℕ} :
↑n = 0 ↔ Even n
source
@[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`.

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

Alias of the reverse direction of `ZMod.natCast_eq_zero_iff_even`.

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

Alias of the reverse direction of `ZMod.intCast_eq_one_iff_odd`.

source
theorem ZMod.natCast_eq_one_iff_odd {n : ℕ} :
↑n = 1 ↔ Odd n
source
@[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`.

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

Alias of the reverse direction of `ZMod.natCast_eq_one_iff_odd`.

source
theorem ZMod.natCast_ne_zero_iff_odd {n : ℕ} :
↑n ≠ 0 ↔ Odd n
source
@[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`.

source
theorem ZMod.coe_mul_inv_eq_one {n : ℕ} (x : ℕ) (h : x.Coprime n) :
↑x * (↑x)⁻¹ = 1
source
theorem ZMod.mul_val_inv {m n : ℕ} (hmn : m.Coprime n) :
↑m * ↑(↑m)⁻¹.val = 1
source
theorem ZMod.val_inv_mul {m n : ℕ} (hmn : m.Coprime n) :
↑(↑m)⁻¹.val * ↑m = 1
source
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`

Equations

- ZMod.unitOfCoprime x h = { val := ↑x, inv := (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ }

Instances For

source
@[simp]
theorem ZMod.coe_unitOfCoprime {n : ℕ} (x : ℕ) (h : x.Coprime n) :
↑(unitOfCoprime x h) = ↑x
source
theorem ZMod.val_coe_unit_coprime {n : ℕ} (u : (ZMod n)ˣ) :
(↑u).val.Coprime n
source
theorem ZMod.isUnit_iff_coprime (m n : ℕ) :
IsUnit ↑m ↔ m.Coprime n
source
theorem ZMod.isUnit_prime_iff_not_dvd {n p : ℕ} (hp : Nat.Prime p) :
IsUnit ↑p ↔ ¬p ∣ n
source
theorem ZMod.isUnit_prime_of_not_dvd {n p : ℕ} (hp : Nat.Prime p) (h : ¬p ∣ n) :
IsUnit ↑p
source
@[simp]
theorem ZMod.inv_coe_unit {n : ℕ} (u : (ZMod n)ˣ) :
(↑u)⁻¹ = ↑u⁻¹
source
theorem ZMod.mul_inv_of_unit {n : ℕ} (a : ZMod n) (h : IsUnit a) :
a * a⁻¹ = 1
source
theorem ZMod.inv_mul_of_unit {n : ℕ} (a : ZMod n) (h : IsUnit a) :
a⁻¹ * a = 1
source
theorem ZMod.inv_eq_of_mul_eq_one (n : ℕ) (a b : ZMod n) (h : a * b = 1) :
a⁻¹ = b
source
@[simp]
theorem ZMod.inv_neg_one (n : ℕ) :
(-1)⁻¹ = -1
source
theorem ZMod.inv_mul_eq_one_of_isUnit {n : ℕ} {a : ZMod n} (ha : IsUnit a) (b : ZMod n) :
a⁻¹ * b = 1 ↔ a = b
source
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`

Equations

- ZMod.unitsEquivCoprime = { toFun := fun (x : (ZMod n)ˣ) => ⟨↑x, ⋯⟩, invFun := fun (x : { x : ZMod n // x.val.Coprime n }) => ZMod.unitOfCoprime (↑x).val ⋯, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem ZMod.subsingleton_iff {n : ℕ} :
Subsingleton (ZMod n) ↔ n = 1
source
theorem ZMod.nontrivial_iff {n : ℕ} :
Nontrivial (ZMod n) ↔ n ≠ 1
source
instance ZMod.subsingleton_units :
Subsingleton (ZMod 2)ˣ
source
@[simp]
theorem ZMod.add_self_eq_zero_iff_eq_zero {n : ℕ} (hn : Odd n) {a : ZMod n} :
a + a = 0 ↔ a = 0
source
theorem ZMod.ne_neg_self {n : ℕ} (hn : Odd n) {a : ZMod n} (ha : a ≠ 0) :
a ≠ -a
source
theorem ZMod.neg_one_ne_one {n : ℕ} [Fact (2 < n)] :
-1 ≠ 1
source
@[simp]
theorem ZMod.neg_eq_self_mod_two (a : ZMod 2) :
-a = a
source
@[simp]
theorem ZMod.intCast_abs_mod_two (a : ℤ) :
↑|a| = ↑a
source
theorem ZMod.natAbs_mod_two (a : ℤ) :
↑a.natAbs = ↑a
source
theorem ZMod.val_ne_zero {n : ℕ} (a : ZMod n) :
a.val ≠ 0 ↔ a ≠ 0
source
@[simp]
theorem ZMod.val_pos {n : ℕ} {a : ZMod n} :
0 < a.val ↔ a ≠ 0
source
theorem ZMod.val_eq_one {n : ℕ} :
1 < n → ∀ (a : ZMod n), a.val = 1 ↔ a = 1
source
theorem ZMod.neg_eq_self_iff {n : ℕ} (a : ZMod n) :
-a = a ↔ a = 0 ∨ 2 * a.val = n
source
theorem ZMod.val_cast_of_lt {n a : ℕ} (h : a < n) :
(↑a).val = a
source
theorem ZMod.val_cast_zmod_lt {m : ℕ} [NeZero m] (n : ℕ) [NeZero n] (a : ZMod m) :
a.cast.val < m
source
theorem ZMod.neg_val' {n : ℕ} [NeZero n] (a : ZMod n) :
(-a).val = (n - a.val) % n
source
theorem ZMod.neg_val {n : ℕ} [NeZero n] (a : ZMod n) :
(-a).val = if a = 0 then 0 else n - a.val
source
theorem ZMod.val_neg_of_ne_zero {n : ℕ} [nz : NeZero n] (a : ZMod n) [na : NeZero a] :
(-a).val = n - a.val
source
theorem ZMod.val_sub {n : ℕ} [NeZero n] {a b : ZMod n} (h : b.val ≤ a.val) :
(a - b).val = a.val - b.val
source
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
source
theorem ZMod.cast_cast_zmod_of_le {m n : ℕ} [hm : NeZero m] (h : m ≤ n) (a : ZMod m) :
a.cast.cast = a
source
theorem ZMod.val_pow {m n : ℕ} {a : ZMod n} [ilt : Fact (1 < n)] (h : a.val ^ m < n) :
(a ^ m).val = a.val ^ m
source
theorem ZMod.val_pow_le {m n : ℕ} [Fact (1 < n)] {a : ZMod n} :
(a ^ m).val ≤ a.val ^ m
source
theorem ZMod.natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : ↑x = ↑y) (hl : x.natAbs ≤ n / 2) :
x.natAbs ≤ y.natAbs
source
theorem RingHom.ext_zmod {n : ℕ} {R : Type u_1} [NonAssocSemiring R] (f g : ZMod n →+* R) :
f = g
source
instance ZMod.subsingleton_ringHom {n : ℕ} {R : Type u_1} [Semiring R] :
Subsingleton (ZMod n →+* R)
source
instance ZMod.subsingleton_ringEquiv {n : ℕ} {R : Type u_1} [Semiring R] :
Subsingleton (ZMod n ≃+* R)
source
@[simp]
theorem ZMod.ringHom_map_cast {n : ℕ} {R : Type u_1} [NonAssocRing R] (f : R →+* ZMod n) (k : ZMod n) :
f k.cast = k
source
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.

source
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.

source
@[simp]
theorem ZMod.castHom_self {n : ℕ} :
castHom ⋯ (ZMod n) = RingHom.id (ZMod n)
source
@[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)
source
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`.

Equations

- ZMod.lift n = (Equiv.subtypeEquivRight ⋯).trans ((Int.castAddHom (ZMod n)).liftOfRightInverse ZMod.cast ⋯)

Instances For

source
@[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
source
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
source
@[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
source
@[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
source
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.

source
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
source
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`.

source
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
Equations

- AddSubgroupClass.instZModSMul = { smul := fun (a : ZMod n) (x : ↥K) => ⟨a • ↑x, ⋯⟩ }

source
@[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
source
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
Equations

- AddSubgroupClass.instZModModule = { toSMul := AddSubgroupClass.instZModSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

source
theorem ZModModule.char_nsmul_eq_zero (n : ℕ) {G : Type u_2} [AddCommGroup G] [Module (ZMod n) G] (x : G) :
n • x = 0
source
theorem ZModModule.char_ne_one (n : ℕ) (G : Type u_2) [AddCommGroup G] [Module (ZMod n) G] [Nontrivial G] :
n ≠ 1
source
theorem ZModModule.two_le_char (n : ℕ) (G : Type u_2) [AddCommGroup G] [Module (ZMod n) G] [NeZero n] [Nontrivial G] :
2 ≤ n
source
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
source
theorem ZModModule.add_self {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] (x : G) :
x + x = 0
source
theorem ZModModule.neg_eq_self {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] (x : G) :
-x = x
source
theorem ZModModule.sub_eq_add {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] (x y : G) :
x - y = x + y
source
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
source
@[simp]
theorem pow_zmod_val_inv_pow {α : Type u_1} [Group α] {n : ℕ} (hn : (Nat.card α).gcd n = 1) (a : α) :
(a ^ (↑n)⁻¹.val) ^ n = a
source
@[simp]
theorem nsmul_zmod_val_inv_nsmul {α : Type u_1} [AddGroup α] {n : ℕ} (hn : (Nat.card α).gcd n = 1) (a : α) :
n • (↑n)⁻¹.val • a = a
source
@[simp]
theorem pow_pow_zmod_val_inv {α : Type u_1} [Group α] {n : ℕ} (hn : (Nat.card α).gcd n = 1) (a : α) :
(a ^ n) ^ (↑n)⁻¹.val = a
source
@[simp]
theorem zmod_val_inv_nsmul_nsmul {α : Type u_1} [AddGroup α] {n : ℕ} (hn : (Nat.card α).gcd n = 1) (a : α) :
(↑n)⁻¹.val • n • a = a
source
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`.

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

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

Equations

- N.residueClassesEquiv = { toFun := fun (n : ℕ) => (↑n, n / N), invFun := fun (p : ZMod N × ℕ) => p.1.val + N * p.2, left_inv := ⋯, right_inv := ⋯ }

Instances For