Simple ring and fields

Main results

• IsSimpleRing.center_isField: the center of a simple ring is a field.
• isSimpleRing_iff_isField: a commutative ring is simple if and only if it is a field.

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

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