Theorem IsSimpleRing.iff_injective_ringHom

Modification history

2024-11-08 19:01
Mathlib/RingTheory/SimpleRing/Basic.lean
feat(RingTheory/SimpleRing/Basic): characterise simple ring in terms of injectiveness (#18113)
Added IsSimpleRing.iff_injective_ringHomView on Github →