Commit 2021-06-22 16:26 9c4afb11

feat(data/zmod): equivalence between the quotient type ℤ / aℤ and zmod a (#7976) This PR defines the equivalence between zmod a and ℤ / aℤ, where a : ℕ or a : ℤ, and the quotient is a quotient group or quotient ring. It also defines zmod.lift n f hf : zmod n →+ A induced by an additive hom f : ℤ →+ A such that f n = 0. (The latter map could be, but is no longer, defined as the composition of the equivalence with quotient.lift f.) Zulip threads:

• (ideal.span {d}).quotient is zmod d
• Homomorphism from the integers descends to $$\mathbb{Z}/n$$
• ∈ gmultiples iff divides