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 #
zmod.quotient_zmultiples_nat_equiv_zmod
andzmod.quotient_zmultiples_equiv_zmod
:zmod n
is the group quotient ofℤ
byn ℤ := add_subgroup.zmultiples (n)
, (wheren : ℕ
andn : ℤ
respectively)zmod.quotient_span_nat_equiv_zmod
andzmod.quotient_span_equiv_zmod
:zmod n
is the ring quotient ofℤ
byn ℤ : ideal.span {n}
(wheren : ℕ
andn : ℤ
respectively)zmod.lift n f
is the map fromzmod n
induced byf : ℤ →+ A
that mapsn
to0
.
Tags #
zmod, quotient group, quotient ring, ideal quotient
ℤ
modulo multiples of n : ℕ
is zmod n
.
ℤ
modulo multiples of a : ℤ
is zmod a.nat_abs
.
ℤ
modulo the ideal generated by n : ℕ
is zmod n
.
ℤ
modulo the ideal generated by a : ℤ
is zmod a.nat_abs
.
Equations
The quotient (ℤ ∙ a) ⧸ (stabilizer b)
is cyclic of order minimal_period ((+ᵥ) a) b
.
Equations
- add_action.zmultiples_quotient_stabilizer_equiv a b = (add_equiv.of_bijective (quotient_add_group.map (add_subgroup.zmultiples ↑(function.minimal_period (has_vadd.vadd ⟨a, _⟩) b)) (add_action.stabilizer ↥(add_subgroup.zmultiples a) b) (⇑(zmultiples_hom ↥(add_subgroup.zmultiples a)) ⟨a, _⟩) _) _).symm.trans (int.quotient_zmultiples_nat_equiv_zmod (function.minimal_period (has_vadd.vadd a) b))
The quotient (a ^ ℤ) ⧸ (stabilizer b)
is cyclic of order minimal_period ((•) a) b
.
Equations
- mul_action.zpowers_quotient_stabilizer_equiv a b = let f : ↥(add_subgroup.zmultiples (⇑additive.of_mul a)) ⧸ add_action.stabilizer ↥(add_subgroup.zmultiples (⇑additive.of_mul a)) b ≃+ zmod (function.minimal_period (has_vadd.vadd (⇑additive.of_mul a)) b) := add_action.zmultiples_quotient_stabilizer_equiv (⇑additive.of_mul a) b in {to_fun := f.to_fun, inv_fun := f.inv_fun, left_inv := _, right_inv := _, map_mul' := _}
The orbit (a ^ ℤ) • b
is a cycle of order minimal_period ((•) a) b
.
The orbit (ℤ • a) +ᵥ b
is a cycle of order minimal_period ((+ᵥ) a) b
.
See also add_order_eq_card_zmultiples
.
See also order_eq_card_zpowers
.