Theorem TwoSidedIdeal.ker_ringCon_mk'

Modification history

2024-11-14 06:25

Mathlib/RingTheory/TwoSidedIdeal/Kernel.lean

refactor(RingHom.injective): use simple ring (#18868)

Modified TwoSidedIdeal.ker_ringCon_mk'View on Github →

2024-11-08 19:01

Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

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

Added TwoSidedIdeal.ker_ringCon_mk'View on Github →