English
For a local ideal I and any element x in R, either x lies in jacobson(I) or there exists y with yx − 1 ∈ I.
Русский
Для локального идеала I и любого элемента x в R либо x лежит в jacobson(I), либо существует y такие, что yx − 1 ∈ I.
LaTeX
$$∀ x, x ∈ jacobson(I) ∨ ∃ y, y * x - 1 ∈ I$$
Lean4
theorem mem_jacobson_or_exists_inv {I : Ideal R} (hi : IsLocal I) (x : R) : x ∈ jacobson I ∨ ∃ y, y * x - 1 ∈ I :=
by_cases
(fun h : I ⊔ span { x } = ⊤ =>
let ⟨p, hpi, q, hq, hpq⟩ := Submodule.mem_sup.1 ((eq_top_iff_one _).1 h)
let ⟨r, hr⟩ := mem_span_singleton.1 hq
Or.inr ⟨r, by rw [← hpq, mul_comm, ← hr, ← neg_sub, add_sub_cancel_right]; exact I.neg_mem hpi⟩)
fun h : I ⊔ span { x } ≠ ⊤ =>
Or.inl <| le_trans le_sup_right (hi.le_jacobson le_sup_left h) <| mem_span_singleton.2 <| dvd_refl x
