quotientZMultiplesEquivZMod — Mathlib

English

For a ∈ ℤ, the quotient ℤ modulo zmultiples(a) is AddEquiv to ZMod(a.natAbs).

Русский

Для a ∈ ℤ, тождество 'ℤ мод zmultiples(a) эквивалентно ZMod(a.natAbs)'.

LaTeX

$$$ \mathbb{Z} / \mathrm{zmultiples}(a) \cong_+ ZMod(a.natAbs) $$$

Lean4

/-- `ℤ` modulo multiples of `a : ℤ` is `ZMod a.natAbs`. -/
def quotientZMultiplesEquivZMod (a : ℤ) : ℤ ⧸ AddSubgroup.zmultiples a ≃+ ZMod a.natAbs :=
  (quotientAddEquivOfEq (zmultiples_natAbs a)).symm.trans (quotientZMultiplesNatEquivZMod a.natAbs)

Похожие утверждения