quotientSpanNatEquivZMod_comp_Quotient_mk

English

For every natural number n, the natural reduction map modulo n composed with the canonical isomorphism to ZMod n equals the canonical embedding Z → ZMod n.

Русский

Для каждого натурального n естественный редукционный отображение по модулю n, затем каноническое изоморождение к ZMod n, совпадают с каноническим вложением Z → ZMod n.

LaTeX

$$$$ (\\mathbb{Z} \\to \\mathbb{Z}/(n) ) \\;\\text{followed by} \\; (\\mathbb{Z}/(n) \\cong \\mathrm{ZMod}\\, n) = \\mathbb{Z} \\xrightarrow{\\mathrm{cast}} \\mathrm{ZMod}\\, n. $$$$

Lean4

@[simp]
theorem quotientSpanNatEquivZMod_comp_Quotient_mk (n : ℕ) :
    (Int.quotientSpanNatEquivZMod n : _ →+* _).comp (Ideal.Quotient.mk (Ideal.span {(n : ℤ)})) =
      Int.castRingHom (ZMod n) :=
  rfl

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