quotientSpanNatEquivZMod_comp_castRingHom

English

For any integer n, the composition of the quotient by the span of n with the ZMod equivalence gives the canonical cast into ZMod |n|.

Русский

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

LaTeX

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

Lean4

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

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