isSimpleRing — Mathlib

English

Every division ring is simple as a ring (the only two‑sided ideals are {0} and the whole ring).

Русский

Любое дивизиональное кольцо простое в смысле кольца: единственные двусторонние идеалы — {0} и всё кольцо.

LaTeX

$$If A is a division ring, then IsSimpleRing A holds; equivalently, the only two‑sided ideals are ⊥ and ⊤.$$

Lean4

instance _root_.DivisionRing.isSimpleRing (A : Type*) [DivisionRing A] : IsSimpleRing A :=
  .of_eq_bot_or_eq_top <| fun I ↦ by
    rw [or_iff_not_imp_left, ← I.one_mem_iff]
    intro H
    obtain ⟨x, hx1, hx2 : x ≠ 0⟩ := SetLike.exists_of_lt (bot_lt_iff_ne_bot.mpr H : ⊥ < I)
    simpa [inv_mul_cancel₀ hx2] using I.mul_mem_left x⁻¹ _ hx1

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