# ZMod n and quotient groups / rings #

This file relates ZMod n to the quotient group ℤ / AddSubgroup.zmultiples (n : ℤ) and to the quotient ring ℤ ⧸ Ideal.span {(n : ℤ)}.

## Main definitions #

• ZMod.quotientZMultiplesNatEquivZMod and ZMod.quotientZMultiplesEquivZMod: ZMod n is the group quotient of ℤ by n ℤ := AddSubgroup.zmultiples (n), (where n : ℕ and n : ℤ respectively)
• ZMod.quotient_span_nat_equiv_zmod and ZMod.quotientSpanEquivZMod : ZMod n is the ring quotient of ℤ by n ℤ : Ideal.span {n} (where n : ℕ and n : ℤ respectively)
• ZMod.lift n f is the map from ZMod n induced by f : ℤ →+ A that maps n to 0.

## Tags #

zmod, quotient group, quotient ring, ideal quotient

ℤ modulo multiples of n : ℕ is ZMod n.

Equations
Instances For

ℤ modulo multiples of a : ℤ is ZMod a.natAbs.

Equations
• a.quotientZMultiplesEquivZMod = .trans ()
Instances For

ℤ modulo the ideal generated by n : ℕ is ZMod n.

Equations
• = .symm.trans
Instances For

ℤ modulo the ideal generated by a : ℤ is ZMod a.natAbs.

Equations
Instances For
def ZMod.prodEquivPi {ι : Type u_3} [] (a : ι) (coprime : Pairwise fun (i j : ι) => (a i).Coprime (a j)) :
ZMod (Finset.univ.prod fun (i : ι) => a i) ≃+* ((i : ι) → ZMod (a i))

The Chinese remainder theorem, elementary version for ZMod. See also Mathlib.Data.ZMod.Basic for versions involving only two numbers.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def AddAction.zmultiplesQuotientStabilizerEquiv {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) :
≃+ ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)

The quotient (ℤ ∙ a) ⧸ (stabilizer b) is cyclic of order minimalPeriod (a +ᵥ ·) b.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) (n : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) :
.symm n = n.cast a,
noncomputable def MulAction.zpowersQuotientStabilizerEquiv {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) :
() ≃* Multiplicative (ZMod (Function.minimalPeriod (fun (x : β) => a x) b))

The quotient (a ^ ℤ) ⧸ (stabilizer b) is cyclic of order minimalPeriod ((•) a) b.

Equations
Instances For
theorem MulAction.zpowersQuotientStabilizerEquiv_symm_apply {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) (n : ZMod (Function.minimalPeriod (fun (x : β) => a x) b)) :
.symm n = a, ^ n.cast
noncomputable def MulAction.orbitZPowersEquiv {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) :
(MulAction.orbit (()) b) ZMod (Function.minimalPeriod (fun (x : β) => a x) b)

The orbit (a ^ ℤ) • b is a cycle of order minimalPeriod ((•) a) b.

Equations
• = .trans .toEquiv
Instances For
noncomputable def AddAction.orbitZMultiplesEquiv {α : Type u_5} {β : Type u_6} [] (a : α) [] (b : β) :
() ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)

The orbit (ℤ • a) +ᵥ b is a cycle of order minimalPeriod (a +ᵥ ·) b.

Equations
• = .trans .toEquiv
Instances For
theorem AddAction.orbitZMultiplesEquiv_symm_apply {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) (k : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) :
.symm k = k.cast a, +ᵥ b,
theorem MulAction.orbitZPowersEquiv_symm_apply {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) (k : ZMod (Function.minimalPeriod (fun (x : β) => a x) b)) :
.symm k = a, ^ k.cast b,
theorem AddAction.orbit_zmultiples_equiv_symm_apply {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) (k : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) :
.symm k = k.cast a, +ᵥ b,

Alias of AddAction.orbitZMultiplesEquiv_symm_apply.

theorem MulAction.orbitZPowersEquiv_symm_apply' {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) (k : ) :
.symm k = a, ^ k b,
theorem AddAction.orbitZMultiplesEquiv_symm_apply' {α : Type u_5} {β : Type u_6} [] (a : α) [] (b : β) (k : ) :
.symm k = k a, +ᵥ b,
theorem AddAction.minimalPeriod_eq_card {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) [Fintype ()] :
Function.minimalPeriod (fun (x : β) => a +ᵥ x) b = Fintype.card ()
theorem MulAction.minimalPeriod_eq_card {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) [Fintype (MulAction.orbit (()) b)] :
Function.minimalPeriod (fun (x : β) => a x) b = Fintype.card (MulAction.orbit (()) b)
instance AddAction.minimalPeriod_pos {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) [Finite ()] :
NeZero (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)
Equations
• =
instance MulAction.minimalPeriod_pos {α : Type u_3} {β : Type u_4} [] (a : α) [] (b : β) [Finite (MulAction.orbit (()) b)] :
NeZero (Function.minimalPeriod (fun (x : β) => a x) b)
Equations
• =
@[simp]
theorem Nat.card_zmultiples {α : Type u_3} [] (a : α) :

See also Fintype.card_zmultiples.

@[simp]
theorem Nat.card_zpowers {α : Type u_3} [] (a : α) :
=

See also Fintype.card_zpowers.

@[simp]
theorem finite_zmultiples {α : Type u_3} [] {a : α} :
().Finite
@[simp]
theorem finite_zpowers {α : Type u_3} [] {a : α} :
(()).Finite
@[simp]
theorem infinite_zmultiples {α : Type u_3} [] {a : α} :
().Infinite
@[simp]
theorem infinite_zpowers {α : Type u_3} [] {a : α} :
(()).Infinite
theorem IsOfFinOrder.finite_zpowers {α : Type u_3} [] {a : α} :
(()).Finite

Alias of the reverse direction of finite_zpowers.

theorem IsOfFinAddOrder.finite_zmultiples {α : Type u_3} [] {a : α} :
().Finite