le_jacobson — Mathlib

English

If I is local, and I ≤ J with J ≠ ⊤, then J ≤ jacobson(I).

Русский

Если I локальный и I ⊆ J с J ≠ ⊤, то J ⊆ jacobson(I).

LaTeX

$$IsLocal(I) → (I ≤ J ∧ J ≠ ⊤) → J ≤ jacobson(I)$$

Lean4

theorem le_jacobson {I J : Ideal R} (hi : IsLocal I) (hij : I ≤ J) (hj : J ≠ ⊤) : J ≤ jacobson I :=
  let ⟨_, hm, hjm⟩ := exists_le_maximal J hj
  le_trans hjm <| le_of_eq <| Eq.symm <| hi.1.eq_of_le hm.1.1 <| sInf_le ⟨le_trans hij hjm, hm⟩

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