Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-21 10:07 de20a394

View on Github →

feat(group_theory/subroup,ring_theory/ideal/operations): lift_of_surjective (#3888) Surjective homomorphisms behave like quotient maps

Estimated changes

Modified src/group_theory/abelianization.lean

Modified src/group_theory/presented_group.lean

Modified src/group_theory/quotient_group.lean

Modified src/group_theory/subgroup.lean

added theorem monoid_hom.eq_lift_of_surjective

added theorem monoid_hom.lift_of_surjective_comp

added theorem monoid_hom.lift_of_surjective_comp_apply

modified theorem monoid_hom.mem_ker

Modified src/ring_theory/ideal/operations.lean

added theorem ring_hom.eq_lift_of_surjective

added theorem ring_hom.lift_of_surjective_comp

added theorem ring_hom.lift_of_surjective_comp_apply