Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ring_hom.lift_injective_of_ker_le_ideal

Modification history

2023-03-02 07:01
src/ring_theory/ideal/operations.lean
refactor(ring_theory/ideal/operations): split quotients to a new file (#18531) …
Modified ring_hom.lift_injective_of_ker_le_idealView on Github →
2022-10-19 07:41
src/ring_theory/ideal/operations.lean
feat(number_theory/kummer_dedekind): define conductor and add basic API plus theorem (#16833) …
Added ring_hom.lift_injective_of_ker_le_idealView on Github →