Commit 2024-02-14 08:30 fabcf9d9

View on Github →

feat(Algebra/Group): Miscellaneous lemmas (#9387) From LeanAPAP, LeanCamCombi and PFR

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

added theorem eq_iff_eq_of_mul_eq_mul

added theorem ne_iff_ne_of_mul_eq_mul

Modified Mathlib/Algebra/Group/Equiv/Basic.lean

added theorem MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm

modified theorem MulEquiv.coe_monoidHom_refl

added theorem MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom

modified theorem MulEquiv.coe_monoidHom_trans

modified theorem MulEquiv.coe_toMonoidHom

added theorem MulEquiv.comp_left_injective

added theorem MulEquiv.comp_right_injective

modified theorem MulEquiv.map_ne_one_iff

modified theorem MulEquiv.ofBijective_apply_symm_apply

modified def MulEquiv.toMonoidHom

modified theorem MulEquiv.toMonoidHom_injective

Modified Mathlib/Algebra/Group/Hom/Basic.lean

added theorem MonoidHom.comp_div

modified theorem MonoidHom.comp_inv

modified theorem MonoidHom.comp_mul

modified theorem MonoidHom.div_apply

added theorem MonoidHom.div_comp

modified theorem MonoidHom.inv_apply

modified theorem MonoidHom.inv_comp

modified theorem MonoidHom.mul_apply

modified theorem MonoidHom.mul_comp

Modified Mathlib/Algebra/Group/Hom/Defs.lean

added theorem map_comp_div'

added theorem map_comp_div

added theorem map_comp_inv

added theorem map_comp_mul

added theorem map_comp_mul_inv

added theorem map_comp_one

added theorem map_comp_pow

added theorem map_comp_zpow'

added theorem map_comp_zpow

Modified Mathlib/Algebra/Group/TypeTags.lean

added theorem AddMonoidHom.coe_toMultiplicative''

added theorem AddMonoidHom.coe_toMultiplicative'

added theorem AddMonoidHom.coe_toMultiplicative

added theorem MonoidHom.coe_toAdditive''

added theorem MonoidHom.coe_toAdditive'

added theorem MonoidHom.coe_toMultiplicative

Modified Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean