of_eq_bot_or_eq_top — Mathlib

English

Let R be a nontrivial ring. If every two‑sided ideal I of R satisfies I = ⊥ or I = ⊤, then R is simple.

Русский

Пусть R — ненулевое кольцо. Если каждый двусторонний идеал I выполняет I = ⊥ или I = ⊤, то R простое.

LaTeX

$$[Nontrivial R] and (for all I : TwoSidedIdeal R, I = ⊥ ∨ I = ⊤) implies IsSimpleRing R.$$

Lean4

theorem of_eq_bot_or_eq_top [Nontrivial R] (h : ∀ I : TwoSidedIdeal R, I = ⊥ ∨ I = ⊤) : IsSimpleRing R where
  simple.eq_bot_or_eq_top := h

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