isJacobsonRing_of_finiteType — Mathlib

English

If A → B is a finite-type ring homomorphism from a Jacobson ring A, then B is Jacobson.

Русский

Если A → B является гомоморфизмом конечного типа из кольца Якобсона A, то B тоже Якобсон.

LaTeX

$$IsJacobsonRing B$$

Lean4

theorem isJacobsonRing_of_finiteType {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [IsJacobsonRing A]
    [Algebra.FiniteType A B] : IsJacobsonRing B :=
  by
  obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_›
  exact isJacobsonRing_of_surjective ⟨f.toRingHom, hf⟩

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