Basic Properties of Simple rings

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

Main results

• IsSimpleRing.nontrivial: simple rings are non-trivial.
• DivisionRing.IsSimpleRing: division rings are simple.
• IsSimpleRing.center_isField: the center of a simple ring is a field.

instance IsSimpleRing.instIsSimpleOrderTwoSidedIdeal {R : Type u_1} [NonUnitalNonAssocRing R] [IsSimpleRing R] : IsSimpleOrder (TwoSidedIdeal R)

Equations

• ⋯ = ⋯

instance IsSimpleRing.instNontrivial {R : Type u_1} [NonUnitalNonAssocRing R] [simple : IsSimpleRing R] : Nontrivial R

Equations

• ⋯ = ⋯

theorem IsSimpleRing.one_mem_of_ne_bot {A : Type u_2} [NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A) (hI : I ≠ ⊥) : 1 ∈ I

theorem IsSimpleRing.one_mem_of_ne_zero_mem {A : Type u_2} [NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A) {x : A} (hx : x ≠ 0) (hxI : x ∈ I) : 1 ∈ I

theorem IsSimpleRing.of_eq_bot_or_eq_top {R : Type u_1} [NonUnitalNonAssocRing R] [Nontrivial R] (h : ∀ (I : TwoSidedIdeal R), I = ⊥ ∨ I = ⊤) : IsSimpleRing R

instance DivisionRing.isSimpleRing (A : Type u_2) [DivisionRing A] : IsSimpleRing A

Equations

• ⋯ = ⋯

theorem IsSimpleRing.isField_center (A : Type u_2) [Ring A] [IsSimpleRing A] : IsField ↥(Subring.center A)

theorem isSimpleRing_iff_isField (A : Type u_2) [CommRing A] : IsSimpleRing A ↔ IsField A