quotient — Mathlib

English

If A is integral over R, then R ↦ A ⟮I⟯ induces an integral extension from R/ I.comap(algebraMap R A) to A/I.

Русский

Если A интегральна над R, тогда переход R/ I comap(algebraMap R A) → A/I образует интегральное расширение.

LaTeX

$$$ {I : Ideal A} \\ [Algebra.IsIntegral R A] : Algebra.IsIntegral (R \\!\\! / I{.comap (algebraMap R A)}) (A / I)$$$

Lean4

instance quotient {I : Ideal A} [Algebra.IsIntegral R A] : Algebra.IsIntegral (R ⧸ I.comap (algebraMap R A)) (A ⧸ I) :=
  ⟨RingHom.IsIntegral.quotient (algebraMap R A) Algebra.IsIntegral.isIntegral⟩

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