mathlib3 documentation

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 #

Tags #

zmod, quotient group, quotient ring, ideal quotient

source
def int.quotient_zmultiples_nat_equiv_zmod (n : ℕ) :
ℤ ⧸ add_subgroup.zmultiples ↑n ≃+ zmod n

ℤ modulo multiples of n : ℕ is zmod n.

Equations
source
def int.quotient_zmultiples_equiv_zmod (a : ℤ) :
ℤ ⧸ add_subgroup.zmultiples a ≃+ zmod a.nat_abs

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

Equations
source
def int.quotient_span_nat_equiv_zmod (n : ℕ) :
ℤ ⧸ ideal.span {↑n} ≃+* zmod n

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

Equations
source
def int.quotient_span_equiv_zmod (a : ℤ) :
ℤ ⧸ ideal.span {a} ≃+* zmod a.nat_abs

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

Equations
source
noncomputable def add_action.zmultiples_quotient_stabilizer_equiv {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [add_action α β] (b : β) :
↥(add_subgroup.zmultiples a) ⧸ add_action.stabilizer ↥(add_subgroup.zmultiples a) b ≃+ zmod (function.minimal_period (has_vadd.vadd a) b)

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

Equations
source
theorem add_action.zmultiples_quotient_stabilizer_equiv_symm_apply {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [add_action α β] (b : β) (n : zmod (function.minimal_period (has_vadd.vadd a) b)) :
⇑((add_action.zmultiples_quotient_stabilizer_equiv a b).symm) n = ↑n • ↑⟨a, _⟩
source
noncomputable def mul_action.zpowers_quotient_stabilizer_equiv {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) :
↥(subgroup.zpowers a) ⧸ mul_action.stabilizer ↥(subgroup.zpowers a) b ≃* multiplicative (zmod (function.minimal_period (has_smul.smul a) b))

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

Equations
source
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)) :
⇑((mul_action.zpowers_quotient_stabilizer_equiv a b).symm) n = ↑⟨a, _⟩ ^ ↑n
source
noncomputable def mul_action.orbit_zpowers_equiv {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) :
↥(mul_action.orbit ↥(subgroup.zpowers a) b) ≃ zmod (function.minimal_period (has_smul.smul a) b)

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

Equations
source
noncomputable def add_action.orbit_zmultiples_equiv {α : Type u_1} {β : Type u_2} [add_group α] (a : α) [add_action α β] (b : β) :
↥(add_action.orbit ↥(add_subgroup.zmultiples a) b) ≃ zmod (function.minimal_period (has_vadd.vadd a) b)

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

Equations
source
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)) :
⇑((mul_action.orbit_zpowers_equiv a b).symm) k = ⟨a, _⟩ ^ ↑k • ⟨b, _⟩
source
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)) :
⇑((add_action.orbit_zmultiples_equiv a b).symm) k = ↑k • ⟨a, _⟩ +ᵥ ⟨b, _⟩
source
theorem mul_action.orbit_zpowers_equiv_symm_apply' {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) (k : ℤ) :
⇑((mul_action.orbit_zpowers_equiv a b).symm) ↑k = ⟨a, _⟩ ^ k • ⟨b, _⟩
source
theorem add_action.orbit_zmultiples_equiv_symm_apply' {α : Type u_1} {β : Type u_2} [add_group α] (a : α) [add_action α β] (b : β) (k : ℤ) :
⇑((add_action.orbit_zmultiples_equiv a b).symm) ↑k = k • ⟨a, _⟩ +ᵥ ⟨b, _⟩
source
theorem add_action.minimal_period_eq_card {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [add_action α β] (b : β) [fintype ↥(add_action.orbit ↥(add_subgroup.zmultiples a) b)] :
function.minimal_period (has_vadd.vadd a) b = fintype.card ↥(add_action.orbit ↥(add_subgroup.zmultiples a) b)
source
theorem mul_action.minimal_period_eq_card {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) [fintype ↥(mul_action.orbit ↥(subgroup.zpowers a) b)] :
function.minimal_period (has_smul.smul a) b = fintype.card ↥(mul_action.orbit ↥(subgroup.zpowers a) b)
source
@[protected, instance]
def add_action.minimal_period_pos {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [add_action α β] (b : β) [finite ↥(add_action.orbit ↥(add_subgroup.zmultiples a) b)] :
ne_zero (function.minimal_period (has_vadd.vadd a) b)
source
@[protected, instance]
def mul_action.minimal_period_pos {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) [finite ↥(mul_action.orbit ↥(subgroup.zpowers a) b)] :
ne_zero (function.minimal_period (has_smul.smul a) b)
source
theorem add_order_eq_card_zmultiples' {α : Type u_3} [add_group α] (a : α) :
add_order_of a = nat.card ↥(add_subgroup.zmultiples a)

See also add_order_eq_card_zmultiples.

source
theorem order_eq_card_zpowers' {α : Type u_3} [group α] (a : α) :
order_of a = nat.card ↥(subgroup.zpowers a)

See also order_eq_card_zpowers.

source
theorem is_of_fin_order.finite_zpowers {α : Type u_3} [group α] {a : α} (h : is_of_fin_order a) :
finite ↥(subgroup.zpowers a)
source
theorem is_of_fin_add_order.finite_zmultiples {α : Type u_3} [add_group α] {a : α} (h : is_of_fin_add_order a) :
finite ↥(add_subgroup.zmultiples a)