Commit 2024-11-08 19:01 3159264f

View on Github →

feat(RingTheory/SimpleRing/Basic): characterise simple ring in terms of injectiveness (#18113)

Estimated changes

Modified Mathlib/RingTheory/SimpleRing/Basic.lean

added theorem IsSimpleRing.iff_injective_ringHom

added theorem IsSimpleRing.iff_injective_ringHom_or_subsingleton_codomain

added theorem IsSimpleRing.injective_ringHom

added theorem IsSimpleRing.injective_ringHom_or_subsingleton_codomain

Modified Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

added theorem TwoSidedIdeal.ker_eq_bot

added theorem TwoSidedIdeal.ker_ringCon_mk'