jacobson_eq_top_iff — Mathlib

English

The Jacobson radical of I equals the top if and only if I equals the top: Jac(I) = ⊤ ⇔ I = ⊤.

Русский

Радикал Якобиана I равен вершине тогда и только тогда, когда I равен вершине: Jac(I) = ⊤ ⇔ I = ⊤.

LaTeX

$$$\operatorname{jacobson}(I) = \top \iff I = \top$$$

Lean4

@[simp]
theorem jacobson_eq_top_iff : jacobson I = ⊤ ↔ I = ⊤ :=
  ⟨fun H =>
    by_contradiction fun hi =>
      let ⟨M, hm, him⟩ := exists_le_maximal I hi
      lt_top_iff_ne_top.1 (lt_of_le_of_lt (show jacobson I ≤ M from sInf_le ⟨him, hm⟩) <| lt_top_iff_ne_top.2 hm.ne_top)
        H,
    fun H => eq_top_iff.2 <| le_sInf fun _ ⟨hij, _⟩ => H ▸ hij⟩

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