isJacobsonRing_iso — Mathlib

English

Let e be a ring isomorphism between R and S. Then R is a Jacobson ring if and only if S is a Jacobson ring.

Русский

Пусть e является кольцевым изоморфизмом между кольцами R и S. Тогда R — кольцо Якобсона тогда и только тогда, когда S — кольцо Якобсона.

LaTeX

$$$IsJacobsonRing(R) \\iff IsJacobsonRing(S)$$$

Lean4

theorem isJacobsonRing_iso (e : R ≃+* S) : IsJacobsonRing R ↔ IsJacobsonRing S
    where
  mp _ := isJacobsonRing_of_surjective ⟨(e : R →+* S), e.surjective⟩
  mpr _ := isJacobsonRing_of_surjective ⟨(e.symm : S →+* R), e.symm.surjective⟩

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