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 #

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

def int.quotient_zmultiples_nat_equiv_zmod (n : ℕ) :

ℤ ⧸ add_subgroup.zmultiples ↑n ≃+ zmod n

ℤ modulo multiples of n : ℕ is zmod n.

Equations

int.quotient_zmultiples_nat_equiv_zmod n = (quotient_add_group.equiv_quotient_of_eq _).symm.trans (quotient_add_group.quotient_ker_equiv_of_right_inverse (int.cast_add_hom (zmod n)) coe zmod.int_cast_zmod_cast)

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

a.quotient_zmultiples_equiv_zmod = (quotient_add_group.equiv_quotient_of_eq _).symm.trans (int.quotient_zmultiples_nat_equiv_zmod a.nat_abs)

def int.quotient_span_nat_equiv_zmod (n : ℕ) :

ℤ ⧸ ideal.span {↑n} ≃+* zmod n

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

Equations

int.quotient_span_nat_equiv_zmod n = (ideal.quot_equiv_of_eq _).symm.trans (ring_hom.quotient_ker_equiv_of_right_inverse _)

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

a.quotient_span_equiv_zmod = (ideal.quot_equiv_of_eq _).symm.trans (int.quotient_span_nat_equiv_zmod a.nat_abs)