Theorem IsSimpleRing.one_mem_of_ne_bot

Modification history

2024-09-19 20:23

Mathlib/RingTheory/SimpleRing/Basic.lean

feat: definition of a simple ring (#14503)

Added IsSimpleRing.one_mem_of_ne_bot View on Github →