quotientSpanNatEquivZMod — Mathlib

English

The quotient of ℤ by the span of n is ring-equivalent to ZMod n.

Русский

Квартира ℤ по идеалу порождаемому n эквивалентна кольце ZMod n.

LaTeX

$$$ \mathbb{Z} \,/\; \operatorname{Ideal.span}\{n\} \cong_+ ZMod(n) $$$

Lean4

/-- `ℤ` modulo the ideal generated by `n : ℕ` is `ZMod n`. -/
def quotientSpanNatEquivZMod : ℤ ⧸ Ideal.span {(n : ℤ)} ≃+* ZMod n :=
  (Ideal.quotEquivOfEq (ZMod.ker_intCastRingHom _)).symm.trans <|
    RingHom.quotientKerEquivOfRightInverse <|
      show Function.RightInverse ZMod.cast (Int.castRingHom (ZMod n)) from intCast_zmod_cast

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