Theorem IsSimpleRing.iff_injective_ringHom_or_subsingleton_codomain

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