Theorem TwoSidedIdeal.ker_eq_bot

Modification history

2024-11-14 06:25
Mathlib/RingTheory/TwoSidedIdeal/Kernel.lean
refactor(RingHom.injective): use simple ring (#18868)
Modified TwoSidedIdeal.ker_eq_botView 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_eq_botView on Github →