mathlib

9c4afb11 - feat(data/zmod): equivalence between the quotient type ℤ / aℤ and `zmod a` (#7976)

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`](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60.28ideal.2Espan.20.7Bd.7D.29.2Equotient.60.20is.20.60zmod.20d.60) - [Homomorphism from the integers descends to $$\mathbb{Z}/n$$](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Homomorphism.20from.20the.20integers.20descends.20to.20.24.24.5Cmathbb.7BZ.7D.2Fn.24.24) - [ `∈ gmultiples` iff divides](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60.E2.88.88.20gmultiples.60.20iff.20divides) Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>