quotient — Mathlib

English

If f: R → S is integral, then the quotient map S → S/I is integral for any ideal I of S.

Русский

Если f: R → S интегральна, то для любого идеала I в S переходная карта S → S/I также интегральна.

LaTeX

$$$f:\\,R\\to S \\text{ integral} \\Rightarrow (\\text{Ideal.quotientMap } I\\, f \\;\\text{le\_rfl}).IsIntegral$$$

Lean4

theorem quotient {I : Ideal S} (hf : f.IsIntegral) : (Ideal.quotientMap I f le_rfl).IsIntegral :=
  by
  rintro ⟨x⟩
  obtain ⟨p, p_monic, hpx⟩ := hf x
  refine ⟨p.map (Ideal.Quotient.mk _), p_monic.map _, ?_⟩
  simpa only [hom_eval₂, eval₂_map] using congr_arg (Ideal.Quotient.mk I) hpx

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