quotientSpanEquivZMod_comp_Quotient_mk

English

For any integer n, the composition of the quotient by span{n} with the quotient equivalence to ZMod n.natAbs equals the canonical cast to ZMod n.natAbs.

Русский

Для целого n композиция деления по span{n} с эквививкой к ZMod n.natAbs равна каноническому отображению в ZMod n.natAbs.

LaTeX

$$$$ (Int.quotientSpanEquivZMod n : _ →+* _).comp (Ideal.Quotient.mk (Ideal.span { (n : \\mathbb{Z}) })) = Int.castRingHom (\\mathbb{Z} / n.\\natAbs \\mathbb{Z}) $$$$

Lean4

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

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