isJacobsonRing_polynomial_iff_isJacobsonRing

English

IsJacobsonRing of the polynomial ring is equivalent to IsJacobsonRing of the base ring.

Русский

Свойство Якобсона кольца полиномов эквивалентно этому свойству базового кольца.

LaTeX

$$$IsJacobsonRing(R[X]) \\iff IsJacobsonRing(R)$$$

Lean4

theorem isJacobsonRing_polynomial_iff_isJacobsonRing : IsJacobsonRing R[X] ↔ IsJacobsonRing R :=
  by
  refine ⟨?_, isJacobsonRing_polynomial_of_isJacobsonRing⟩
  intro H
  exact
    isJacobsonRing_of_surjective
      ⟨eval₂RingHom (RingHom.id _) 1, fun x => ⟨C x, by simp only [coe_eval₂RingHom, RingHom.id_apply, eval₂_C]⟩⟩

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