quotientSpanEquivZMod_comp_castRingHom

English

The composition of the inverse span-equivalence with the natural cast from ZMod |n| to itself equals the quotient map by span{n}.

Русский

Обратная часть изоморфии по Span и естественное отображение порождают эквивалентность к квотерованию по span{n}.

LaTeX

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

Lean4

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

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