Theorem TwoSidedIdeal.ker_ringCon

Modification history

2024-11-14 06:25
Mathlib/RingTheory/TwoSidedIdeal/Kernel.lean
refactor(RingHom.injective): use simple ring (#18868)
Added TwoSidedIdeal.ker_ringConView on Github →