# mathlib3documentation

data.zmod.quotient

# zmod n and quotient groups / rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file relates zmod n to the quotient group quotient_add_group.quotient (add_subgroup.zmultiples n) and to the quotient ring (ideal.span {n}).quotient.

## Main definitions #

• zmod.quotient_zmultiples_nat_equiv_zmod and zmod.quotient_zmultiples_equiv_zmod: zmod n is the group quotient of ℤ by n ℤ := add_subgroup.zmultiples (n), (where n : ℕ and n : ℤ respectively)
• zmod.quotient_span_nat_equiv_zmod and zmod.quotient_span_equiv_zmod: 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

ℤ modulo multiples of a : ℤ is zmod a.nat_abs.

Equations

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

Equations

ℤ modulo the ideal generated by a : ℤ is zmod a.nat_abs.

Equations
noncomputable def add_action.zmultiples_quotient_stabilizer_equiv {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [ β] (b : β) :

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

Equations
theorem add_action.zmultiples_quotient_stabilizer_equiv_symm_apply {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [ β] (b : β) (n : zmod ) :
= n a, _⟩
noncomputable def mul_action.zpowers_quotient_stabilizer_equiv {α : Type u_3} {β : Type u_4} [group α] (a : α) [ β] (b : β) :

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

Equations
theorem mul_action.zpowers_quotient_stabilizer_equiv_symm_apply {α : Type u_3} {β : Type u_4} [group α] (a : α) [ β] (b : β) (n : zmod ) :
= a, _⟩ ^ n
noncomputable def mul_action.orbit_zpowers_equiv {α : Type u_3} {β : Type u_4} [group α] (a : α) [ β] (b : β) :

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

Equations
noncomputable def add_action.orbit_zmultiples_equiv {α : Type u_1} {β : Type u_2} [add_group α] (a : α) [ β] (b : β) :

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

Equations
theorem mul_action.orbit_zpowers_equiv_symm_apply {α : Type u_3} {β : Type u_4} [group α] (a : α) [ β] (b : β) (k : zmod ) :
.symm) k = a, _⟩ ^ k b, _⟩
theorem add_action.orbit_zmultiples_equiv_symm_apply {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [ β] (b : β) (k : zmod ) :
k = k a, _⟩ +ᵥ b, _⟩
theorem mul_action.orbit_zpowers_equiv_symm_apply' {α : Type u_3} {β : Type u_4} [group α] (a : α) [ β] (b : β) (k : ) :
.symm) k = a, _⟩ ^ k b, _⟩
theorem add_action.orbit_zmultiples_equiv_symm_apply' {α : Type u_1} {β : Type u_2} [add_group α] (a : α) [ β] (b : β) (k : ) :
k = k a, _⟩ +ᵥ b, _⟩
theorem add_action.minimal_period_eq_card {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [ β] (b : β)  :
theorem mul_action.minimal_period_eq_card {α : Type u_3} {β : Type u_4} [group α] (a : α) [ β] (b : β) [fintype ] :
@[protected, instance]
def add_action.minimal_period_pos {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [ β] (b : β)  :
@[protected, instance]
def mul_action.minimal_period_pos {α : Type u_3} {β : Type u_4} [group α] (a : α) [ β] (b : β) [finite ] :
theorem add_order_eq_card_zmultiples' {α : Type u_3} [add_group α] (a : α) :

See also add_order_eq_card_zmultiples.

theorem order_eq_card_zpowers' {α : Type u_3} [group α] (a : α) :

See also order_eq_card_zpowers.

theorem is_of_fin_order.finite_zpowers {α : Type u_3} [group α] {a : α} (h : is_of_fin_order a) :