Module docstring
{"# 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.
"}
IsSimpleRing
structure
(R : Type*) [NonUnitalNonAssocRing R]
Full source
/--
A ring `R` is **simple** if it has only two two-sided ideals, namely `⊥` and `⊤`.
-/
@[mk_iff] class IsSimpleRing (R : Type*) [NonUnitalNonAssocRing R] : Prop where
simple : IsSimpleOrder (TwoSidedIdeal R)Informal description
A ring $R$ is called *simple* if it has exactly two two-sided ideals: the zero ideal $\{0\}$ (denoted $\bot$) and the entire ring $R$ itself (denoted $\top$).