Simple rings

A ring R is simple if it has only two two-sided ideals, namely ⊥ and ⊤.

Main definitions

• IsSimpleRing: a predicate expressing that a ring is simple.

class IsSimpleRing (R : Type u_1) [NonUnitalNonAssocRing R] : Prop

A ring R is simple if it has only two two-sided ideals, namely ⊥ and ⊤.

• simple : IsSimpleOrder (TwoSidedIdeal R)

theorem IsSimpleRing.simple {R : Type u_1} : ∀ {inst : NonUnitalNonAssocRing R} [self : IsSimpleRing R], IsSimpleOrder (TwoSidedIdeal R)