# 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
• valMinAbs returns the integer closest to zero 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

Equations
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
Instances For
theorem ZMod.val_lt {n : } [] (a : ZMod n) :
a.val < n
theorem ZMod.val_le {n : } [] (a : ZMod n) :
a.val n
@[simp]
theorem ZMod.val_zero {n : } :
= 0
@[simp]
theorem ZMod.val_one' :
= 1
@[simp]
theorem ZMod.val_neg' {n : ZMod 0} :
(-n).val = n.val
@[simp]
theorem ZMod.val_mul' {m : ZMod 0} {n : ZMod 0} :
(m * n).val = m.val * n.val
@[simp]
theorem ZMod.val_natCast {n : } (a : ) :
(a).val = a % n
theorem ZMod.val_unit' {n : ZMod 0} :
n.val = 1
theorem ZMod.eq_one_of_isUnit_natCast {n : } (h : IsUnit n) :
n = 1
theorem ZMod.val_natCast_of_lt {n : } {a : } (h : a < n) :
(a).val = a
instance ZMod.charP (n : ) :
CharP (ZMod n) n
Equations
• =
@[simp]
theorem ZMod.addOrderOf_one (n : ) :
= n
@[simp]
theorem ZMod.addOrderOf_coe (a : ) {n : } (n0 : n 0) :
= 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) :
= 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 : ) :

We have that ringChar (ZMod n) = n.

theorem ZMod.natCast_self (n : ) :
n = 0
@[simp]
theorem ZMod.natCast_self' (n : ) :
n + 1 = 0
def ZMod.cast {R : Type u_1} [] {n : } :
ZMod nR

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 = match (motive := (x : ) → ZMod xR) x with | 0 => Int.cast | n.succ => fun (i : ZMod (n + 1)) => i.val
Instances For
@[simp]
theorem ZMod.cast_zero {n : } {R : Type u_1} [] :
= 0
theorem ZMod.cast_eq_val {n : } {R : Type u_1} [] [] (a : ZMod n) :
a.cast = a.val
@[simp]
theorem Prod.fst_zmod_cast {n : } {R : Type u_1} [] {S : Type u_2} [] (a : ZMod n) :
a.cast.1 = a.cast
@[simp]
theorem Prod.snd_zmod_cast {n : } {R : Type u_1} [] {S : Type u_2} [] (a : ZMod n) :
a.cast.2 = a.cast
theorem ZMod.natCast_zmod_val {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 : } [] :
Function.RightInverse ZMod.val 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.cast_id (n : ) (i : ZMod n) :
i.cast = i
@[simp]
theorem ZMod.cast_id' {n : } :
ZMod.cast = id
@[simp]
theorem ZMod.natCast_comp_val {n : } (R : Type u_1) [Ring R] [] :
Nat.cast ZMod.val = ZMod.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 ZMod.cast = ZMod.cast

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

@[simp]
theorem ZMod.natCast_val {n : } {R : Type u_1} [Ring R] [] (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 : ZMod n) (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) :
= 1
theorem ZMod.cast_add {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (b : ZMod n) :
(a + b).cast = a.cast + b.cast
theorem ZMod.cast_mul {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (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] :

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.

Equations
• = { toFun := ZMod.cast, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem ZMod.castHom_apply {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] {h : m n} (i : ZMod n) :
() i = i.cast
@[simp]
theorem ZMod.cast_sub {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (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

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

@[simp]
theorem ZMod.cast_one' {n : } {R : Type u_1} [Ring R] [CharP R n] :
= 1
@[simp]
theorem ZMod.cast_add' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (b : ZMod n) :
(a + b).cast = a.cast + b.cast
@[simp]
theorem ZMod.cast_mul' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (b : ZMod n) :
(a * b).cast = a.cast * b.cast
@[simp]
theorem ZMod.cast_sub' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (b : ZMod n) :
(a - b).cast = a.cast - b.cast
@[simp]
theorem ZMod.cast_pow' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (k : ) :
(a ^ k).cast = a.cast ^ k
@[simp]
theorem ZMod.cast_natCast' {n : } {R : Type u_1} [Ring R] [CharP R n] (k : ) :
(k).cast = k
@[simp]
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] :
theorem ZMod.castHom_bijective {n : } (R : Type u_1) [Ring R] [CharP R n] [] (h : ) :
noncomputable def ZMod.ringEquiv {n : } (R : Type u_1) [Ring R] [CharP R n] [] (h : ) :

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

Equations
Instances For
def ZMod.ringEquivCongr {m : } {n : } (h : m = 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
@[simp]
theorem ZMod.ringEquivCongr_refl_apply {a : } (x : ZMod a) :
x = x
theorem ZMod.ringEquivCongr_symm {a : } {b : } (hab : a = b) :
().symm =
theorem ZMod.ringEquivCongr_trans {a : } {b : } {c : } (hab : a = b) (hbc : b = c) :
().trans () =
theorem ZMod.ringEquivCongr_ringEquivCongr_apply {a : } {b : } {c : } (hab : a = b) (hbc : b = c) (x : ZMod a) :
() (() x) = x
theorem ZMod.ringEquivCongr_val {a : } {b : } (h : a = b) (x : ZMod a) :
( x).val = x.val
theorem ZMod.int_coe_ringEquivCongr {a : } {b : } (h : a = b) (z : ) :
z = z
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.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_zmod_eq_zero_iff_dvd (a : ) (b : ) :
a = 0 b a
theorem ZMod.val_intCast {n : } (a : ) [] :
(a).val = a % n
theorem ZMod.coe_intCast {n : } (a : ) :
(a).cast = a % 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.nat_coe_zmod_eq_iff (p : ) (n : ) (z : ZMod p) [] :
n = z ∃ (k : ), n = z.val + p * k
theorem ZMod.int_coe_zmod_eq_iff (p : ) (n : ) (z : ZMod p) [] :
n = z ∃ (k : ), n = z.val + p * k
@[simp]
theorem ZMod.intCast_mod (a : ) (b : ) :
(a % b) = a
theorem ZMod.ker_intCastAddHom (n : ) :
().ker =
theorem ZMod.cast_injective_of_le {m : } {n : } [nzm : ] (h : m n) :
theorem ZMod.cast_zmod_eq_zero_iff_of_le {m : } {n : } [] (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_one_eq_one_mod (n : ) :
= 1 % n
theorem ZMod.val_one (n : ) [Fact (1 < n)] :
= 1
theorem ZMod.val_add {n : } [] (a : ZMod n) (b : ZMod n) :
(a + b).val = (a.val + b.val) % n
theorem ZMod.val_add_of_lt {n : } {a : ZMod n} {b : ZMod n} (h : a.val + b.val < n) :
(a + b).val = a.val + b.val
theorem ZMod.val_add_val_of_le {n : } [] {a : ZMod n} {b : ZMod n} (h : n a.val + b.val) :
a.val + b.val = (a + b).val + n
theorem ZMod.val_add_of_le {n : } [] {a : ZMod n} {b : ZMod n} (h : n a.val + b.val) :
(a + b).val = a.val + b.val - n
theorem ZMod.val_add_le {n : } (a : ZMod n) (b : ZMod n) :
(a + b).val a.val + b.val
theorem ZMod.val_mul {n : } (a : ZMod n) (b : ZMod n) :
(a * b).val = a.val * b.val % n
theorem ZMod.val_mul_le {n : } (a : ZMod n) (b : ZMod n) :
(a * b).val a.val * b.val
theorem ZMod.val_mul_of_lt {n : } {a : ZMod n} {b : ZMod n} (h : a.val * b.val < n) :
(a * b).val = a.val * b.val
instance ZMod.nontrivial (n : ) [Fact (1 < n)] :
Equations
• =
Equations
def ZMod.inv (n : ) :
ZMod nZMod 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 x✝ x = match x✝, x with | 0, i => | n.succ, i => (i.val.gcdA (n + 1))
Instances For
instance ZMod.instInv (n : ) :
Inv (ZMod n)
Equations
• = { inv := }
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.natCast_mod (a : ) (n : ) :
(a % n) = a
theorem ZMod.eq_iff_modEq_nat (n : ) {a : } {b : } :
a = b a b [MOD n]
theorem ZMod.coe_mul_inv_eq_one {n : } (x : ) (h : x.Coprime n) :
x * (x)⁻¹ = 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

Equations
• = { val := x, inv := (x)⁻¹, val_inv := , inv_val := }
Instances For
@[simp]
theorem ZMod.coe_unitOfCoprime {n : } (x : ) (h : x.Coprime n) :
() = 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
theorem ZMod.isUnit_prime_iff_not_dvd {n : } {p : } (hp : p.Prime) :
IsUnit p ¬p n
theorem ZMod.isUnit_prime_of_not_dvd {n : } {p : } (hp : p.Prime) (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 : ) :
a * a⁻¹ = 1
theorem ZMod.inv_mul_of_unit {n : } (a : ZMod n) (h : ) :
a⁻¹ * a = 1
theorem ZMod.inv_eq_of_mul_eq_one (n : ) (a : ZMod n) (b : ZMod n) (h : a * b = 1) :
a⁻¹ = b
def ZMod.unitsEquivCoprime {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
• One or more equations did not get rendered due to their size.
Instances For
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
Equations
@[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.natAbs_mod_two (a : ) :
a.natAbs = a
@[simp]
theorem ZMod.val_eq_zero {n : } (a : ZMod n) :
a.val = 0 a = 0
theorem ZMod.val_ne_zero {n : } (a : ZMod n) :
a.val 0 a 0
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.neg_val' {n : } [] (a : ZMod n) :
(-a).val = (n - a.val) % n
theorem ZMod.neg_val {n : } [] (a : ZMod n) :
(-a).val = if a = 0 then 0 else n - a.val
theorem ZMod.val_neg_of_ne_zero {n : } [nz : ] (a : ZMod n) [na : ] :
(-a).val = n - a.val
theorem ZMod.val_sub {n : } [] {a : ZMod n} {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 : ] {a : ZMod m} (h : a.val < n) :
a.cast.val = a.val
theorem ZMod.cast_cast_zmod_of_le {m : } {n : } [hm : ] (h : m n) (a : ZMod m) :
a.cast.cast = a
def ZMod.valMinAbs {n : } :
ZMod n

valMinAbs x returns the integer in the same equivalence class as x that is closest to 0, The result will be in the interval (-n/2, n/2].

Equations
• x.valMinAbs = match x✝, x with | 0, x => x | n@h:n_1.succ, x => if x.val n / 2 then x.val else x.val - n
Instances For
@[simp]
theorem ZMod.valMinAbs_def_zero (x : ZMod 0) :
x.valMinAbs = x
theorem ZMod.valMinAbs_def_pos {n : } [] (x : ZMod n) :
x.valMinAbs = if x.val n / 2 then x.val else x.val - n
@[simp]
theorem ZMod.coe_valMinAbs {n : } (x : ZMod n) :
x.valMinAbs = x
theorem Nat.le_div_two_iff_mul_two_le {n : } {m : } :
m n / 2 m * 2 n
theorem ZMod.valMinAbs_nonneg_iff {n : } [] (x : ZMod n) :
0 x.valMinAbs x.val n / 2
theorem ZMod.valMinAbs_mul_two_eq_iff {n : } (a : ZMod n) :
a.valMinAbs * 2 = n 2 * a.val = n
theorem ZMod.valMinAbs_mem_Ioc {n : } [] (x : ZMod n) :
x.valMinAbs * 2 Set.Ioc (-n) n
theorem ZMod.valMinAbs_spec {n : } [] (x : ZMod n) (y : ) :
x.valMinAbs = y x = y y * 2 Set.Ioc (-n) n
theorem ZMod.natAbs_valMinAbs_le {n : } [] (x : ZMod n) :
x.valMinAbs.natAbs n / 2
@[simp]
theorem ZMod.valMinAbs_zero (n : ) :
@[simp]
theorem ZMod.valMinAbs_eq_zero {n : } (x : ZMod n) :
x.valMinAbs = 0 x = 0
theorem ZMod.natCast_natAbs_valMinAbs {n : } [] (a : ZMod n) :
a.valMinAbs.natAbs = if a.val n / 2 then a else -a
theorem ZMod.valMinAbs_neg_of_ne_half {n : } {a : ZMod n} (ha : 2 * a.val n) :
(-a).valMinAbs = -a.valMinAbs
@[simp]
theorem ZMod.natAbs_valMinAbs_neg {n : } (a : ZMod n) :
(-a).valMinAbs.natAbs = a.valMinAbs.natAbs
theorem ZMod.val_eq_ite_valMinAbs {n : } [] (a : ZMod n) :
a.val = a.valMinAbs + (if a.val n / 2 then 0 else n)
theorem ZMod.prime_ne_zero (p : ) (q : ) [hp : Fact p.Prime] [hq : Fact q.Prime] (hpq : p q) :
q 0
theorem ZMod.valMinAbs_natAbs_eq_min {n : } [hpos : ] (a : ZMod n) :
a.valMinAbs.natAbs = min a.val (n - a.val)
theorem ZMod.valMinAbs_natCast_of_le_half {n : } {a : } (ha : a n / 2) :
(a).valMinAbs = a
theorem ZMod.valMinAbs_natCast_of_half_lt {n : } {a : } (ha : n / 2 < a) (ha' : a < n) :
(a).valMinAbs = a - n
@[simp]
theorem ZMod.valMinAbs_natCast_eq_self {n : } {a : } [] :
(a).valMinAbs = a a n / 2
theorem ZMod.natAbs_min_of_le_div_two (n : ) (x : ) (y : ) (he : x = y) (hl : x.natAbs n / 2) :
x.natAbs y.natAbs
theorem ZMod.natAbs_valMinAbs_add_le {n : } (a : ZMod n) (b : ZMod n) :
(a + b).valMinAbs.natAbs (a.valMinAbs + b.valMinAbs).natAbs
instance ZMod.instField (p : ) [Fact p.Prime] :

Field structure on ZMod p if p is prime.

Equations
• = Field.mk zpowRec (fun (q : ℚ≥0) (a : ZMod p) => q * a) (fun (a : ) (x : ZMod p) => a * x)
instance ZMod.instIsDomain (p : ) [hp : Fact p.Prime] :

ZMod p is an integral domain when p is prime.

Equations
• =
theorem RingHom.ext_zmod {n : } {R : Type u_1} [] (f : ZMod n →+* R) (g : ZMod n →+* R) :
f = g
instance ZMod.subsingleton_ringHom {n : } {R : Type u_1} [] :
Equations
• =
instance ZMod.subsingleton_ringEquiv {n : } {R : Type u_1} [] :
Equations
• =
@[simp]
theorem ZMod.ringHom_map_cast {n : } {R : Type u_1} [Ring R] (f : R →+* ZMod n) (k : ZMod n) :
f k.cast = k
theorem ZMod.ringHom_rightInverse {n : } {R : Type u_1} [Ring R] (f : R →+* ZMod n) :
Function.RightInverse ZMod.cast f

Any ring homomorphism into ZMod n has a right inverse.

theorem ZMod.ringHom_surjective {n : } {R : Type u_1} [Ring R] (f : R →+* ZMod n) :

Any ring homomorphism into ZMod n is surjective.

@[simp]
@[simp]
theorem ZMod.castHom_comp {n : } {m : } {d : } (hm : n m) (hd : m d) :
(ZMod.castHom hm (ZMod n)).comp (ZMod.castHom hd (ZMod m)) = ZMod.castHom (ZMod n)
def ZMod.lift (n : ) {A : Type u_2} [] :
{ f : →+ A // f n = 0 } (ZMod n →+ A)

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

Equations
• = .trans (().liftOfRightInverse ZMod.cast )
Instances For
@[simp]
theorem ZMod.lift_coe (n : ) {A : Type u_2} [] (f : { f : →+ A // f n = 0 }) (x : ) :
(() f) x = f x
theorem ZMod.lift_castAddHom (n : ) {A : Type u_2} [] (f : { f : →+ A // f n = 0 }) (x : ) :
(() f) (() x) = f x
@[simp]
theorem ZMod.lift_comp_coe (n : ) {A : Type u_2} [] (f : { f : →+ A // f n = 0 }) :
(() f) Int.cast = f
@[simp]
theorem ZMod.lift_comp_castAddHom (n : ) {A : Type u_2} [] (f : { f : →+ A // f n = 0 }) :
(() f).comp () = f
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.