Commit 2023-01-28 07:11 5157ef07

View on Github →

feat: port Algebra.Hom.Freiman (#1538)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Hom/Freiman.lean

added structure AddFreimanHom

added theorem FreimanHom.FreimanHomClass_of_le

added theorem FreimanHom.cancel_left_on

added theorem FreimanHom.cancel_right

added theorem FreimanHom.cancel_right_on

added theorem FreimanHom.coe_comp

added theorem FreimanHom.coe_mk

added theorem FreimanHom.comp_apply

added theorem FreimanHom.comp_assoc

added theorem FreimanHom.comp_id

added def FreimanHom.const

added theorem FreimanHom.const_apply

added theorem FreimanHom.const_comp

added theorem FreimanHom.div_apply

added theorem FreimanHom.div_comp

added theorem FreimanHom.ext

added theorem FreimanHom.id_comp

added theorem FreimanHom.inv_apply

added theorem FreimanHom.inv_comp

added theorem FreimanHom.mk_coe

added theorem FreimanHom.mul_apply

added theorem FreimanHom.mul_comp

added theorem FreimanHom.one_apply

added theorem FreimanHom.one_comp

added def FreimanHom.toFreimanHom

added theorem FreimanHom.toFreimanHom_coe

added theorem FreimanHom.toFreimanHom_injective

added theorem FreimanHom.to_fun_eq_coe

added structure FreimanHom

added def FreimanHomClass.toFreimanHom

added def MonoidHom.toFreimanHom

added theorem MonoidHom.toFreimanHom_coe

added theorem MonoidHom.toFreimanHom_injective

added theorem map_mul_map_eq_map_mul_map

added theorem map_prod_eq_map_prod

added theorem map_prod_eq_map_prod_of_le

Modified Mathlib/Algebra/Hom/GroupAction.lean