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

instance ZMod.charZero : CharZero (ZMod 0)

Equations

• ZMod.charZero = ⋯

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 = match (motive := (x : ℕ) → ZMod x → ℕ) x with | 0 => Int.natAbs | n.succ => Fin.val

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 : ℕ} : ZMod.val 0 = 0

@[simp]

theorem ZMod.val_one' : ZMod.val 1 = 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} : IsUnit n ↔ 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 : ℕ) : 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

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 = match (motive := (x : ℕ) → ZMod x → R) x with | 0 => Int.cast | n.succ => fun (i : ZMod (n + 1)) => ↑i.val

@[simp]

theorem ZMod.cast_zero {n : ℕ} {R : Type u_1} [AddGroupWithOne R] : ZMod.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 ZMod.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 ZMod.cast Int.cast

theorem ZMod.intCast_surjective {n : ℕ} : Function.Surjective Int.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] [NeZero n] : 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] [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 : 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) : ZMod.cast 1 = 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] : 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.

Equations

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

@[simp]

theorem ZMod.castHom_apply {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] {h : m ∣ n} (i : ZMod n) : (ZMod.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 : 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] : ZMod.cast 1 = 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] : Function.Injective ⇑(ZMod.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 ⇑(ZMod.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.

Equations

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

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.

@[simp]

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

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

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

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

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

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

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

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

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 ↔ c.ModEq a b

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 : ℤ) [NeZero n] : ↑(↑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) [NeZero p] : ↑n = z ↔ ∃ (k : ℕ), n = z.val + p * k

theorem ZMod.int_coe_zmod_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.ker_intCastRingHom (n : ℕ) : RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span {↑n}

theorem ZMod.cast_injective_of_le {m : ℕ} {n : ℕ} [nzm : NeZero m] (h : m ≤ n) : Function.Injective ZMod.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 ZMod.val

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

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

theorem ZMod.val_add {n : ℕ} [NeZero 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 : ℕ} [NeZero 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 : ℕ} [NeZero 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)] : Nontrivial (ZMod n)

Equations

• ⋯ = ⋯

instance ZMod.nontrivial' : Nontrivial (ZMod 0)

Equations

• ZMod.nontrivial' = ⋯

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 x✝ x = match x✝, x with | 0, i => Int.sign i | n.succ, i => ↑(i.val.gcdA (n + 1))

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

Equations

• ZMod.instInv n = { inv := ZMod.inv 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.natCast_mod (a : ℕ) (n : ℕ) : ↑(a % n) = ↑a

theorem ZMod.eq_iff_modEq_nat (n : ℕ) {a : ℕ} {b : ℕ} : ↑a = ↑b ↔ n.ModEq a b

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

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

@[simp]

theorem ZMod.coe_unitOfCoprime {n : ℕ} (x : ℕ) (h : x.Coprime n) : ↑(ZMod.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

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 : 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 : ZMod n) (b : ZMod n) (h : 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

Equations

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

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.

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

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

instance ZMod.subsingleton_units : Subsingleton (ZMod 2)ˣ

Equations

• ZMod.subsingleton_units = ⋯

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

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

@[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 : ℕ} [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 : 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 : 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

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

@[simp]

theorem ZMod.valMinAbs_def_zero (x : ZMod 0) : x.valMinAbs = x

theorem ZMod.valMinAbs_def_pos {n : ℕ} [NeZero 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 ZMod.injective_valMinAbs {n : ℕ} : Function.Injective ZMod.valMinAbs

theorem Nat.le_div_two_iff_mul_two_le {n : ℕ} {m : ℕ} : m ≤ n / 2 ↔ ↑m * 2 ≤ ↑n

theorem ZMod.valMinAbs_nonneg_iff {n : ℕ} [NeZero 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 : ℕ} [NeZero n] (x : ZMod n) : x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n

theorem ZMod.valMinAbs_spec {n : ℕ} [NeZero n] (x : ZMod n) (y : ℤ) : x.valMinAbs = y ↔ x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n

theorem ZMod.natAbs_valMinAbs_le {n : ℕ} [NeZero n] (x : ZMod n) : x.valMinAbs.natAbs ≤ n / 2

@[simp]

theorem ZMod.valMinAbs_zero (n : ℕ) : ZMod.valMinAbs 0 = 0

@[simp]

theorem ZMod.valMinAbs_eq_zero {n : ℕ} (x : ZMod n) : x.valMinAbs = 0 ↔ x = 0

theorem ZMod.natCast_natAbs_valMinAbs {n : ℕ} [NeZero 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 : ℕ} [NeZero 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 : NeZero n] (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 : ℕ} [NeZero n] : (↑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 (ZMod p)

Field structure on ZMod p if p is prime.

Equations

• ZMod.instField p = 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] : IsDomain (ZMod p)

ZMod p is an integral domain when p is prime.

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

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

theorem ZMod.ringHom_eq_of_ker_eq {n : ℕ} {R : Type u_1} [CommRing R] (f : R →+* ZMod n) (g : R →+* ZMod n) (h : RingHom.ker f = RingHom.ker g) : f = g

@[simp]

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

@[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} [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 ⋯)

@[simp]

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

theorem ZMod.lift_castAddHom (n : ℕ) {A : Type u_2} [AddGroup A] (f : { f : ℤ →+ A // f ↑n = 0 }) (x : ℤ) : ((ZMod.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 }) : ⇑((ZMod.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 }) : ((ZMod.lift n) f).comp (Int.castAddHom (ZMod n)) = ↑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.