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.gmultiples 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