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 = (_ : 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 | Nat.succ n => Fin.val

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

theorem ZMod.val_le {n : ℕ} [NeZero n] (a : ZMod n) : ZMod.val a ≤ 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} : ZMod.val (-n) = ZMod.val n

@[simp]

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

@[simp]

theorem ZMod.val_nat_cast {n : ℕ} (a : ℕ) : ZMod.val ↑a = a % n

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

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

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

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

Equations

• (_ : CharP (ZMod n) 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 / Nat.gcd n 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 / Nat.gcd n 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.nat_cast_self (n : ℕ) : ↑n = 0

@[simp]

theorem ZMod.nat_cast_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 | Nat.succ n => fun (i : ZMod (n + 1)) => ↑(ZMod.val i)

@[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) : ZMod.cast a = ↑(ZMod.val a)

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

theorem ZMod.nat_cast_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.int_cast_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.nat_cast_val {n : ℕ} {R : Type u_1} [Ring R] [NeZero n] (i : ZMod n) : ↑(ZMod.val i) = ZMod.cast i

@[simp]

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

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

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) : ZMod.cast (a + b) = ZMod.cast a + ZMod.cast b

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

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

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

@[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 = ZMod.cast i

@[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) : ZMod.cast (a - b) = ZMod.cast a - ZMod.cast b

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ZMod.cast_int_cast {n : ℕ} {R : Type u_1} [Ring R] {m : ℕ} [CharP R m] (h : m ∣ n) (k : ℤ) : ZMod.cast ↑k = ↑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) : ZMod.cast (a + b) = ZMod.cast a + ZMod.cast b

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem ZMod.castHom_injective {n : ℕ} (R : Type u_1) [Ring R] [CharP R n] : Function.Injective ⇑(ZMod.castHom (_ : n ∣ n) 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 (_ : n ∣ n) 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 (_ : n ∣ n) R) (_ : Function.Bijective ⇑(ZMod.castHom (_ : n ∣ n) 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.

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

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

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

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

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

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

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

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

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

@[simp]

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

theorem ZMod.cast_neg_one {R : Type u_1} [Ring R] (n : ℕ) : ZMod.cast (-1) = ↑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) : ZMod.cast (k - 1) = (if k = 0 then ↑n else ZMod.cast k) - 1

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

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

@[simp]

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

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

theorem ZMod.ker_int_castRingHom (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) : ZMod.cast a = 0 ↔ a = 0

@[simp]

theorem ZMod.nat_cast_toNat (p : ℕ) {z : ℤ} (_h : 0 ≤ z) : ↑(Int.toNat z) = ↑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) : ZMod.val (a + b) = (ZMod.val a + ZMod.val b) % n

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

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

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

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

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

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

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

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

Equations

• (_ : Nontrivial (ZMod n)) = (_ : Nontrivial (ZMod n))

instance ZMod.nontrivial' : Nontrivial (ZMod 0)

Equations

• ZMod.nontrivial' = (_ : Nontrivial (ZMod 0))

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 | Nat.succ n, i => ↑(Nat.gcdA (ZMod.val i) (n + 1))

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

Equations

• ZMod.instInvZMod n = { inv := ZMod.inv n }

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

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

@[simp]

theorem ZMod.nat_cast_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 : Nat.Coprime x n) : ↑x * (↑x)⁻¹ = 1

def ZMod.unitOfCoprime {n : ℕ} (x : ℕ) (h : Nat.Coprime x 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 := (_ : ↑x * (↑x)⁻¹ = 1), inv_val := (_ : (↑x)⁻¹ * ↑x = 1) }

@[simp]

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

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

theorem ZMod.isUnit_iff_coprime (m : ℕ) (n : ℕ) : IsUnit ↑m ↔ Nat.Coprime m 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 : ZMod n) (b : ZMod n) (h : a * b = 1) : a⁻¹ = b

def ZMod.unitsEquivCoprime {n : ℕ} [NeZero n] : (ZMod n)ˣ ≃ { x : ZMod n // Nat.Coprime (ZMod.val x) 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 : Nat.Coprime m 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.

instance ZMod.subsingleton_units : Subsingleton (ZMod 2)ˣ

Equations

• ZMod.subsingleton_units = (_ : 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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

theorem ZMod.cast_cast_zmod_of_le {m : ℕ} {n : ℕ} [hm : NeZero m] (h : m ≤ n) (a : ZMod m) : ZMod.cast (ZMod.cast a) = 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

• ZMod.valMinAbs x = match x✝, x with | 0, x => x | n@h:(Nat.succ n_1), x => if ZMod.val x ≤ n / 2 then ↑(ZMod.val x) else ↑(ZMod.val x) - ↑n

@[simp]

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

theorem ZMod.valMinAbs_def_pos {n : ℕ} [NeZero n] (x : ZMod n) : ZMod.valMinAbs x = if ZMod.val x ≤ n / 2 then ↑(ZMod.val x) else ↑(ZMod.val x) - ↑n

@[simp]

theorem ZMod.coe_valMinAbs {n : ℕ} (x : ZMod n) : ↑(ZMod.valMinAbs x) = 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 ≤ ZMod.valMinAbs x ↔ ZMod.val x ≤ n / 2

theorem ZMod.valMinAbs_mul_two_eq_iff {n : ℕ} (a : ZMod n) : ZMod.valMinAbs a * 2 = ↑n ↔ 2 * ZMod.val a = n

theorem ZMod.valMinAbs_mem_Ioc {n : ℕ} [NeZero n] (x : ZMod n) : ZMod.valMinAbs x * 2 ∈ Set.Ioc (-↑n) ↑n

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

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

@[simp]

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

@[simp]

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

theorem ZMod.nat_cast_natAbs_valMinAbs {n : ℕ} [NeZero n] (a : ZMod n) : ↑(Int.natAbs (ZMod.valMinAbs a)) = if ZMod.val a ≤ n / 2 then a else -a

theorem ZMod.valMinAbs_neg_of_ne_half {n : ℕ} {a : ZMod n} (ha : 2 * ZMod.val a ≠ n) : ZMod.valMinAbs (-a) = -ZMod.valMinAbs a

@[simp]

theorem ZMod.natAbs_valMinAbs_neg {n : ℕ} (a : ZMod n) : Int.natAbs (ZMod.valMinAbs (-a)) = Int.natAbs (ZMod.valMinAbs a)

theorem ZMod.val_eq_ite_valMinAbs {n : ℕ} [NeZero n] (a : ZMod n) : ↑(ZMod.val a) = ZMod.valMinAbs a + ↑(if ZMod.val a ≤ n / 2 then 0 else n)

theorem ZMod.prime_ne_zero (p : ℕ) (q : ℕ) [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (hpq : p ≠ q) : ↑q ≠ 0

theorem ZMod.valMinAbs_natAbs_eq_min {n : ℕ} [hpos : NeZero n] (a : ZMod n) : Int.natAbs (ZMod.valMinAbs a) = min (ZMod.val a) (n - ZMod.val a)

theorem ZMod.valMinAbs_natCast_of_le_half {n : ℕ} {a : ℕ} (ha : a ≤ n / 2) : ZMod.valMinAbs ↑a = ↑a

theorem ZMod.valMinAbs_natCast_of_half_lt {n : ℕ} {a : ℕ} (ha : n / 2 < a) (ha' : a < n) : ZMod.valMinAbs ↑a = ↑a - ↑n

@[simp]

theorem ZMod.valMinAbs_natCast_eq_self {n : ℕ} {a : ℕ} [NeZero n] : ZMod.valMinAbs ↑a = ↑a ↔ a ≤ n / 2

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

theorem ZMod.natAbs_valMinAbs_add_le {n : ℕ} (a : ZMod n) (b : ZMod n) : Int.natAbs (ZMod.valMinAbs (a + b)) ≤ Int.natAbs (ZMod.valMinAbs a + ZMod.valMinAbs b)

instance ZMod.instFieldZMod (p : ℕ) [Fact (Nat.Prime p)] : Field (ZMod p)

Field structure on ZMod p if p is prime.

Equations

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

instance ZMod.instIsDomainZModToSemiringToDivisionSemiringToSemifieldInstFieldZMod (p : ℕ) [hp : Fact (Nat.Prime p)] : IsDomain (ZMod p)

ZMod p is an integral domain when p is prime.

Equations

• (_ : IsDomain (ZMod p)) = (_ : IsDomain (ZMod p))

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

• (_ : Subsingleton (ZMod n →+* R)) = (_ : Subsingleton (ZMod n →+* R))

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

Equations

• (_ : Subsingleton (ZMod n ≃+* R)) = (_ : Subsingleton (ZMod n ≃+* R))

@[simp]

theorem ZMod.ringHom_map_cast {n : ℕ} {R : Type u_1} [Ring R] (f : R →+* ZMod n) (k : ZMod n) : f (ZMod.cast k) = 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 (_ : n ∣ n) (ZMod n) = RingHom.id (ZMod n)

@[simp]

theorem ZMod.castHom_comp {n : ℕ} {m : ℕ} {d : ℕ} (hm : n ∣ m) (hd : m ∣ d) : RingHom.comp (ZMod.castHom hm (ZMod n)) (ZMod.castHom hd (ZMod m)) = ZMod.castHom (_ : n ∣ d) (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

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

@[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 }) : AddMonoidHom.comp ((ZMod.lift n) f) (Int.castAddHom (ZMod n)) = ↑f