Theorem IsSimpleRing.one_mem_of_ne_zero_mem

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_zero_memView on Github →