mathlib documentation

data.zmod.quotient

zmod n and quotient groups / rings #

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 #

Tags #

zmod, quotient group, quotient ring, ideal quotient

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

Equations
theorem mul_action.zpowers_quotient_stabilizer_equiv_symm_apply {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) (n : zmod (function.minimal_period (has_smul.smul a) b)) :
noncomputable def mul_action.orbit_zpowers_equiv {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (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 : α) [add_action α β] (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 : α) [mul_action α β] (b : β) (k : zmod (function.minimal_period (has_smul.smul a) b)) :
theorem add_action.orbit_zmultiples_equiv_symm_apply {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [add_action α β] (b : β) (k : zmod (function.minimal_period (has_vadd.vadd a) b)) :
theorem mul_action.orbit_zpowers_equiv_symm_apply' {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) (k : ) :
theorem add_action.orbit_zmultiples_equiv_symm_apply' {α : Type u_1} {β : Type u_2} [add_group α] (a : α) [add_action α β] (b : β) (k : ) :
@[protected, instance]
def add_action.minimal_period_pos {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [add_action α β] (b : β) [fintype (add_action.orbit (add_subgroup.zmultiples a) b)] :
@[protected, instance]
def mul_action.minimal_period_pos {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) [fintype (mul_action.orbit (subgroup.zpowers a) b)] :
theorem order_eq_card_zpowers' {α : Type u_3} [group α] (a : α) :

See also order_eq_card_zpowers.