Commit 2021-03-23 15:29 c2e9ec02

View on Github →

feat(group_theory/subgroup): add {monoid,add_monoid,ring}_hom.lift_of_right_inverse (#6814) This provides a computable alternative to lift_of_surjective.

Estimated changes

Modified src/data/zmod/basic.lean

Modified src/group_theory/subgroup.lean

added theorem monoid_hom.eq_lift_of_right_inverse

deleted theorem monoid_hom.eq_lift_of_surjective

added def monoid_hom.lift_of_right_inverse

added def monoid_hom.lift_of_right_inverse_aux

added theorem monoid_hom.lift_of_right_inverse_aux_comp_apply

added theorem monoid_hom.lift_of_right_inverse_comp

added theorem monoid_hom.lift_of_right_inverse_comp_apply

deleted theorem monoid_hom.lift_of_surjective_comp

deleted theorem monoid_hom.lift_of_surjective_comp_apply

Modified src/ring_theory/ideal/operations.lean

added theorem ring_hom.eq_lift_of_right_inverse

deleted theorem ring_hom.eq_lift_of_surjective

added def ring_hom.lift_of_right_inverse

added def ring_hom.lift_of_right_inverse_aux

added theorem ring_hom.lift_of_right_inverse_aux_comp_apply

added theorem ring_hom.lift_of_right_inverse_comp

added theorem ring_hom.lift_of_right_inverse_comp_apply

deleted theorem ring_hom.lift_of_surjective_comp

deleted theorem ring_hom.lift_of_surjective_comp_apply

Modified src/ring_theory/roots_of_unity.lean

Modified src/ring_theory/witt_vector/truncated.lean