one_mem_of_ne_bot — Mathlib

English

Let A be a simple ring (not necessarily unital). If I is a two‑sided ideal of A with I ≠ ⊥, then 1 ∈ I.

Русский

Пусть A — простое кольцо (не обязательно с единицей). Если I — двусторонний идеал A и I ≠ ⊥, то 1 ∈ I.

LaTeX

$$$\\text{In a simple ring } A,\\ \\forall I\\ \\text{a two‑sided ideal of } A,\\ I \\ne \\bot \\Rightarrow 1 \\in I.$$$

Lean4

theorem one_mem_of_ne_bot {A : Type*} [NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A) (hI : I ≠ ⊥) :
    (1 : A) ∈ I :=
  (eq_bot_or_eq_top I).resolve_left hI ▸ ⟨⟩

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