jacobson_radical_eq_jacobson — Mathlib

English

The Jacobson radical of the radical of an ideal I equals the Jacobson radical of I itself: I.radical.jacobson = I.jacobson.

Русский

Радикал Якобсона радикала идеала I равен радикалу Якобсона самого I: I.radical.jacobson = I.jacobson.

LaTeX

$$$I.\mathrm{radical}.\mathrm{jacobson} = I.\mathrm{jacobson}$$$

Lean4

theorem jacobson_radical_eq_jacobson : I.radical.jacobson = I.jacobson :=
  le_antisymm
    (le_trans (le_of_eq (congr_arg jacobson (radical_eq_sInf I)))
      (sInf_le_sInf fun _ hJ => ⟨sInf_le ⟨hJ.1, hJ.2.isPrime⟩, hJ.2⟩))
    (jacobson_mono le_radical)

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