maximalIdeal_le_jacobson — Mathlib

English

For any ideal I in a local ring R, the maximal ideal m of R is contained in the Jacobson radical of I: m ≤ jacobson(I).

Русский

Для любого идеала I локального кольца R максимальный идеал m принадлежит радикалу Якобсона I: m ⊆ jacobson(I).

LaTeX

$$$ \mathfrak{m} \subseteq I.{\tt jacobson}. $$$

Lean4

theorem maximalIdeal_le_jacobson (I : Ideal R) : IsLocalRing.maximalIdeal R ≤ I.jacobson :=
  le_sInf fun _ ⟨_, h⟩ => le_of_eq (IsLocalRing.eq_maximalIdeal h).symm

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