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

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

ZMod.val 0 = 0

source

@[simp]

theorem ZMod.val_one' :

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

@[deprecated ZMod.val_natCast]

theorem ZMod.val_nat_cast {n : ℕ} (a : ℕ) :

(↑a).val = a % n

Alias of ZMod.val_natCast.

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

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

(↑a).val = a

source

@[deprecated ZMod.val_natCast_of_lt]

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

(↑a).val = a

Alias of ZMod.val_natCast_of_lt.

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

@[deprecated ZMod.natCast_self]

theorem ZMod.nat_cast_self (n : ℕ) :

↑n = 0

Alias of ZMod.natCast_self.

source

@[simp]

theorem ZMod.natCast_self' (n : ℕ) :

↑n + 1 = 0

source

@[deprecated ZMod.natCast_self']

theorem ZMod.nat_cast_self' (n : ℕ) :

↑n + 1 = 0

Alias of ZMod.natCast_self'.

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] :

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

@[deprecated ZMod.natCast_zmod_val]

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

↑a.val = a

Alias of ZMod.natCast_zmod_val.

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 ZMod.val Nat.cast

source

@[deprecated ZMod.natCast_rightInverse]

theorem ZMod.nat_cast_rightInverse {n : ℕ} [NeZero n] :

Function.RightInverse ZMod.val Nat.cast

Alias of ZMod.natCast_rightInverse.

source

theorem ZMod.natCast_zmod_surjective {n : ℕ} [NeZero n] :

Function.Surjective Nat.cast

source

@[deprecated ZMod.natCast_zmod_surjective]

theorem ZMod.nat_cast_zmod_surjective {n : ℕ} [NeZero n] :

Function.Surjective Nat.cast

Alias of ZMod.natCast_zmod_surjective.

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

@[deprecated ZMod.intCast_zmod_cast]

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

↑a.cast = a

Alias of ZMod.intCast_zmod_cast.

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 ZMod.cast Int.cast

source

@[deprecated ZMod.intCast_rightInverse]

theorem ZMod.int_cast_rightInverse {n : ℕ} :

Function.RightInverse ZMod.cast Int.cast

Alias of ZMod.intCast_rightInverse.

source

theorem ZMod.intCast_surjective {n : ℕ} :

Function.Surjective Int.cast

source

@[deprecated ZMod.intCast_surjective]

theorem ZMod.int_cast_surjective {n : ℕ} :

Function.Surjective Int.cast

Alias of ZMod.intCast_surjective.

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

ZMod.cast = id

source

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

source

@[deprecated ZMod.natCast_comp_val]

theorem ZMod.nat_cast_comp_val {n : ℕ} (R : Type u_1) [Ring R] [NeZero n] :

Nat.cast ∘ ZMod.val = ZMod.cast

Alias of ZMod.natCast_comp_val.

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 ∘ ZMod.cast = ZMod.cast

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

source

@[deprecated ZMod.intCast_comp_cast]

theorem ZMod.int_cast_comp_cast {n : ℕ} (R : Type u_1) [Ring R] :

Int.cast ∘ ZMod.cast = ZMod.cast

Alias of ZMod.intCast_comp_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

@[deprecated ZMod.natCast_val]

theorem ZMod.nat_cast_val {n : ℕ} {R : Type u_1} [Ring R] [NeZero n] (i : ZMod n) :

↑i.val = i.cast

Alias of ZMod.natCast_val.

source

@[simp]

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

↑i.cast = i.cast

source

@[deprecated ZMod.intCast_cast]

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

↑i.cast = i.cast

Alias of ZMod.intCast_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) :

ZMod.cast 1 = 1

source

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

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

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) :

(ZMod.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

@[deprecated ZMod.cast_natCast]

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

(↑k).cast = ↑k

Alias of ZMod.cast_natCast.

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

@[deprecated ZMod.cast_intCast]

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

(↑k).cast = ↑k

Alias of ZMod.cast_intCast.

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

source

@[simp]

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

ZMod.cast 1 = 1

source

@[simp]

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

@[simp]

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

@[simp]

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

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

source

@[simp]

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

(↑k).cast = ↑k

source

@[deprecated ZMod.cast_natCast']

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

(↑k).cast = ↑k

Alias of ZMod.cast_natCast'.

source

@[simp]

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

(↑k).cast = ↑k

source

@[deprecated ZMod.cast_intCast']

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

(↑k).cast = ↑k

Alias of ZMod.cast_intCast'.

source

theorem ZMod.castHom_injective {n : ℕ} (R : Type u_1) [Ring R] [CharP R n] :

Function.Injective ⇑(ZMod.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 ⇑(ZMod.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) :

ZMod.ringEquivOfPrime R hp hR = ZMod.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 : ℕ) :

ZMod.ringEquivCongr ⋯ = RingEquiv.refl (ZMod a)

source

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

(ZMod.ringEquivCongr ⋯) x = x

source

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

(ZMod.ringEquivCongr hab).symm = ZMod.ringEquivCongr ⋯

source

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

(ZMod.ringEquivCongr hab).trans (ZMod.ringEquivCongr hbc) = ZMod.ringEquivCongr ⋯

source

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

source

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

((ZMod.ringEquivCongr h) x).val = x.val

source

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

(ZMod.ringEquivCongr h) ↑z = ↑z

source

@[deprecated ZMod.ringEquivCongr_intCast]

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

(ZMod.ringEquivCongr h) ↑z = ↑z

Alias of ZMod.ringEquivCongr_intCast.

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

@[deprecated ZMod.intCast_eq_intCast_iff]

theorem ZMod.int_cast_eq_int_cast_iff (a b : ℤ) (c : ℕ) :

↑a = ↑b ↔ a ≡ b [ZMOD ↑c]

Alias of ZMod.intCast_eq_intCast_iff.

source

theorem ZMod.intCast_eq_intCast_iff' (a b : ℤ) (c : ℕ) :

↑a = ↑b ↔ a % ↑c = b % ↑c

source

@[deprecated ZMod.intCast_eq_intCast_iff']

theorem ZMod.int_cast_eq_int_cast_iff' (a b : ℤ) (c : ℕ) :

↑a = ↑b ↔ a % ↑c = b % ↑c

Alias of ZMod.intCast_eq_intCast_iff'.

source

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

↑(↑a).val = a % ↑n

source

@[deprecated ZMod.val_intCast]

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

↑(↑a).val = a % ↑n

Alias of ZMod.val_intCast.

source

theorem ZMod.natCast_eq_natCast_iff (a b c : ℕ) :

↑a = ↑b ↔ a ≡ b [MOD c]

source

@[deprecated ZMod.natCast_eq_natCast_iff]

theorem ZMod.nat_cast_eq_nat_cast_iff (a b c : ℕ) :

↑a = ↑b ↔ a ≡ b [MOD c]

Alias of ZMod.natCast_eq_natCast_iff.

source

theorem ZMod.natCast_eq_natCast_iff' (a b c : ℕ) :

↑a = ↑b ↔ a % c = b % c

source

@[deprecated ZMod.natCast_eq_natCast_iff']

theorem ZMod.nat_cast_eq_nat_cast_iff' (a b c : ℕ) :

↑a = ↑b ↔ a % c = b % c

Alias of ZMod.natCast_eq_natCast_iff'.

source

theorem ZMod.intCast_zmod_eq_zero_iff_dvd (a : ℤ) (b : ℕ) :

↑a = 0 ↔ ↑b ∣ a

source

@[deprecated ZMod.intCast_zmod_eq_zero_iff_dvd]

theorem ZMod.int_cast_zmod_eq_zero_iff_dvd (a : ℤ) (b : ℕ) :

↑a = 0 ↔ ↑b ∣ a

Alias of ZMod.intCast_zmod_eq_zero_iff_dvd.

source

theorem ZMod.intCast_eq_intCast_iff_dvd_sub (a b : ℤ) (c : ℕ) :

↑a = ↑b ↔ ↑c ∣ b - a

source

@[deprecated ZMod.intCast_eq_intCast_iff_dvd_sub]

theorem ZMod.int_cast_eq_int_cast_iff_dvd_sub (a b : ℤ) (c : ℕ) :

↑a = ↑b ↔ ↑c ∣ b - a

Alias of ZMod.intCast_eq_intCast_iff_dvd_sub.

source

theorem ZMod.natCast_zmod_eq_zero_iff_dvd (a b : ℕ) :

↑a = 0 ↔ b ∣ a

source

@[deprecated ZMod.natCast_zmod_eq_zero_iff_dvd]

theorem ZMod.nat_cast_zmod_eq_zero_iff_dvd (a b : ℕ) :

↑a = 0 ↔ b ∣ a

Alias of ZMod.natCast_zmod_eq_zero_iff_dvd.

source

theorem ZMod.coe_intCast {n : ℕ} (a : ℤ) :

(↑a).cast = a % ↑n

source

@[deprecated ZMod.coe_intCast]

theorem ZMod.coe_int_cast {n : ℕ} (a : ℤ) :

(↑a).cast = a % ↑n

Alias of ZMod.coe_intCast.

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

@[deprecated ZMod.natCast_eq_iff]

theorem ZMod.nat_coe_zmod_eq_iff (p n : ℕ) (z : ZMod p) [NeZero p] :

↑n = z ↔ ∃ (k : ℕ), n = z.val + p * k

Alias of ZMod.natCast_eq_iff.

source

@[deprecated ZMod.intCast_eq_iff]

theorem ZMod.int_coe_zmod_eq_iff (p : ℕ) (n : ℤ) (z : ZMod p) [NeZero p] :

↑n = z ↔ ∃ (k : ℤ), n = ↑z.val + ↑p * k

Alias of ZMod.intCast_eq_iff.

source

@[simp]

theorem ZMod.intCast_mod (a : ℤ) (b : ℕ) :

↑(a % ↑b) = ↑a

source

@[deprecated ZMod.intCast_mod]

theorem ZMod.int_cast_mod (a : ℤ) (b : ℕ) :

↑(a % ↑b) = ↑a

Alias of ZMod.intCast_mod.

source

theorem ZMod.ker_intCastAddHom (n : ℕ) :

(Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples ↑n

source

@[deprecated ZMod.ker_intCastAddHom]

theorem ZMod.ker_int_castAddHom (n : ℕ) :

(Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples ↑n

Alias of ZMod.ker_intCastAddHom.

source

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

Function.Injective ZMod.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

@[deprecated ZMod.natCast_toNat]

theorem ZMod.nat_cast_toNat (p : ℕ) {z : ℤ} (_h : 0 ≤ z) :

↑z.toNat = ↑z

Alias of ZMod.natCast_toNat.

source

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

Function.Injective ZMod.val

source

theorem ZMod.val_one_eq_one_mod (n : ℕ) :

ZMod.val 1 = 1 % n

source

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

ZMod.val 1 = 1

source

theorem ZMod.val_one'' {n : ℕ} :

n ≠ 1 → ZMod.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

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_mod]

theorem ZMod.nat_cast_mod (a n : ℕ) :

↑(a % n) = ↑a

Alias of ZMod.natCast_mod.

source

theorem ZMod.eq_iff_modEq_nat (n : ℕ) {a b : ℕ} :

↑a = ↑b ↔ a ≡ b [MOD n]

source

theorem ZMod.eq_zero_iff_even {n : ℕ} :

↑n = 0 ↔ Even n

source

theorem ZMod.eq_one_iff_odd {n : ℕ} :

↑n = 1 ↔ Odd n

source

theorem ZMod.ne_zero_iff_odd {n : ℕ} :

↑n ≠ 0 ↔ Odd n

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) :

↑(ZMod.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

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

theorem ZMod.neg_eq_self_mod_two (a : ZMod 2) :

-a = a

source

@[simp]

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

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

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_2.valMinAbs = x_2
x_2.valMinAbs = if x_2.val ≤ n.succ / 2 then ↑x_2.val else ↑x_2.val - ↑n.succ

Instances For

source

@[simp]

theorem ZMod.valMinAbs_def_zero (x : ZMod 0) :

x.valMinAbs = x

source

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

source

@[simp]

theorem ZMod.coe_valMinAbs {n : ℕ} (x : ZMod n) :

↑x.valMinAbs = x

source

theorem ZMod.injective_valMinAbs {n : ℕ} :

Function.Injective ZMod.valMinAbs

source

theorem Nat.le_div_two_iff_mul_two_le {n m : ℕ} :

m ≤ n / 2 ↔ ↑m * 2 ≤ ↑n

source

theorem ZMod.valMinAbs_nonneg_iff {n : ℕ} [NeZero n] (x : ZMod n) :

0 ≤ x.valMinAbs ↔ x.val ≤ n / 2

source

theorem ZMod.valMinAbs_mul_two_eq_iff {n : ℕ} (a : ZMod n) :

a.valMinAbs * 2 = ↑n ↔ 2 * a.val = n

source

theorem ZMod.valMinAbs_mem_Ioc {n : ℕ} [NeZero n] (x : ZMod n) :

x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n

source

theorem ZMod.valMinAbs_spec {n : ℕ} [NeZero n] (x : ZMod n) (y : ℤ) :

x.valMinAbs = y ↔ x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n

source

theorem ZMod.natAbs_valMinAbs_le {n : ℕ} [NeZero n] (x : ZMod n) :

x.valMinAbs.natAbs ≤ n / 2

source

@[simp]

theorem ZMod.valMinAbs_zero (n : ℕ) :

ZMod.valMinAbs 0 = 0

source

@[simp]

theorem ZMod.valMinAbs_eq_zero {n : ℕ} (x : ZMod n) :

x.valMinAbs = 0 ↔ x = 0

source

theorem ZMod.natCast_natAbs_valMinAbs {n : ℕ} [NeZero n] (a : ZMod n) :

↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a

source

@[deprecated ZMod.natCast_natAbs_valMinAbs]

theorem ZMod.nat_cast_natAbs_valMinAbs {n : ℕ} [NeZero n] (a : ZMod n) :

↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a

Alias of ZMod.natCast_natAbs_valMinAbs.

source

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

(-a).valMinAbs = -a.valMinAbs

source

@[simp]

theorem ZMod.natAbs_valMinAbs_neg {n : ℕ} (a : ZMod n) :

(-a).valMinAbs.natAbs = a.valMinAbs.natAbs

source

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)

source

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

↑q ≠ 0

source

theorem ZMod.valMinAbs_natAbs_eq_min {n : ℕ} [hpos : NeZero n] (a : ZMod n) :

a.valMinAbs.natAbs = a.val ⊓ (n - a.val)

source

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

(↑a).valMinAbs = ↑a

source

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

(↑a).valMinAbs = ↑a - ↑n

source

@[simp]

theorem ZMod.valMinAbs_natCast_eq_self {n a : ℕ} [NeZero n] :

(↑a).valMinAbs = ↑a ↔ a ≤ n / 2

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 ZMod.natAbs_valMinAbs_add_le {n : ℕ} (a b : ZMod n) :

(a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

source

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

Field (ZMod p)

Field structure on ZMod p if p is prime.

Equations

ZMod.instField p = Field.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x : ℚ≥0) => HMul.hMul ↑x) ⋯ ⋯ (fun (x : ℚ) => HMul.hMul ↑x) ⋯

source

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

IsDomain (ZMod p)

ZMod p is an integral domain when p is prime.

source

theorem RingHom.ext_zmod {n : ℕ} {R : Type u_1} [Semiring 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} [Ring R] (f : R →+* ZMod n) (k : ZMod n) :

f k.cast = k

source

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.

source

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

Function.Surjective ⇑f

Any ring homomorphism into ZMod n is surjective.

source

@[simp]

theorem ZMod.castHom_self {n : ℕ} :

ZMod.castHom ⋯ (ZMod n) = RingHom.id (ZMod n)

source

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

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 : ℤ) :

((ZMod.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 : ℤ) :

((ZMod.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 }) :

⇑((ZMod.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 }) :

((ZMod.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 ⇑((ZMod.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 = Function.Injective.module (ZMod n) (AddSubmonoidClass.subtype K) ⋯ ⋯

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 nsmul_zmod_val_inv_nsmul {α : Type u_1} [AddGroup α] {n : ℕ} (hn : (Nat.card α).Coprime n) (a : α) :

n • (↑n)⁻¹.val • a = a

source

@[simp]

theorem zmod_val_inv_nsmul_nsmul {α : Type u_1} [AddGroup α] {n : ℕ} (hn : (Nat.card α).Coprime n) (a : α) :

(↑n)⁻¹.val • n • a = a

source

@[simp]

theorem pow_zmod_val_inv_pow {α : Type u_1} [Group α] {n : ℕ} (hn : (Nat.card α).Coprime n) (a : α) :

(a ^ (↑n)⁻¹.val) ^ n = a

source

@[simp]

theorem pow_pow_zmod_val_inv {α : Type u_1} [Group α] {n : ℕ} (hn : (Nat.card α).Coprime n) (a : α) :

(a ^ n) ^ (↑n)⁻¹.val = 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

Documentation

Mathlib.Data.ZMod.Basic

Integers mod `n` #

Definitions #

Groups of bounded torsion #

Integers mod n #

Definitions #

Groups of bounded torsion #

Integers mod `n` #