# mathlibdocumentation

data.zmod.quotient

# zmod n and quotient groups / rings #

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

## Main definitions #

• zmod.quotient_gmultiples_nat_equiv_zmod and zmod.quotient_gmultiples_equiv_zmod: zmod n is the group quotient of ℤ by n ℤ := add_subgroup.gmultiples (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