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_iff (R : Type u_1) [NonUnitalNonAssocRing R] : IsSimpleRing R ↔ IsSimpleOrder (TwoSidedIdeal R)