quotientZMultiplesNatEquivZMod — Mathlib

English

There is a natural isomorphism between the integers modulo nℤ and ZMod n.

Русский

Существуют естественные изоморфизмы между εℤ/ nℤ и ZMod n.

LaTeX

$$$ \\mathbb{Z} / n\\mathbb{Z} \\;\cong\\; ZMod(n) $$$

Lean4

/-- `ℤ` modulo multiples of `n : ℕ` is `ZMod n`. -/
def quotientZMultiplesNatEquivZMod : ℤ ⧸ AddSubgroup.zmultiples (n : ℤ) ≃+ ZMod n :=
  (quotientAddEquivOfEq (ZMod.ker_intCastAddHom _)).symm.trans <|
    quotientKerEquivOfRightInverse (Int.castAddHom (ZMod n)) cast intCast_zmod_cast

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