isSimpleRing_iff_isTwoSided_imp — Mathlib

English

For a ring R, IsSimpleRing R holds if and only if R is nontrivial and every ideal I of R satisfies I = ⊥ or I = ⊤.

Русский

Для кольца R справедливо: IsSimpleRing R эквивалентно тому, что R ненулевое и каждый идеал I удовлетворяет I = ⊥ или I = ⊤.

LaTeX

$$IsSimpleRing R ↔ (Nontrivial R ∧ ∀ I : Ideal R, I.IsTwoSided → I = ⊥ ∨ I = ⊤).$$

Lean4

theorem isSimpleRing_iff_isTwoSided_imp {R : Type*} [Ring R] :
    IsSimpleRing R ↔ Nontrivial R ∧ ∀ I : Ideal R, I.IsTwoSided → I = ⊥ ∨ I = ⊤ :=
  by
  let e := orderIsoIsTwoSided (R := R)
  simp_rw [isSimpleRing_iff, isSimpleOrder_iff, orderIsoRingCon.toEquiv.nontrivial_congr, RingCon.nontrivial_iff,
    e.forall_congr_left, Subtype.forall, ← e.injective.eq_iff]
  simp [e, Subtype.ext_iff]

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