isJacobsonRing — Mathlib

English

If f : A → B is a finite-type ring homomorphism and A Jacobson, then B is Jacobson.

Русский

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

LaTeX

$$IsJacobsonRing B$$

Lean4

theorem isJacobsonRing {A B : Type*} [CommRing A] [CommRing B] {f : A →+* B} [IsJacobsonRing A] (H : f.FiniteType) :
    IsJacobsonRing B :=
  @isJacobsonRing_of_finiteType A B _ _ f.toAlgebra _ H

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