Commit 2024-09-19 20:23 c8f01e78

View on Github →

feat: definition of a simple ring (#14503)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/SimpleRing/Basic.lean

added theorem IsSimpleRing.isField_center

added theorem IsSimpleRing.of_eq_bot_or_eq_top

added theorem IsSimpleRing.one_mem_of_ne_bot

added theorem IsSimpleRing.one_mem_of_ne_zero_mem

added theorem isSimpleRing_iff_isField

Created Mathlib/RingTheory/SimpleRing/Defs.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean

added theorem TwoSidedIdeal.one_mem_iff