Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-06 14:41 9b39ab2a

View on Github →

feat(algebra/group/freiman): Freiman homomorphisms (#10497) This defines Freiman homomorphisms, which are maps preserving products of n elements (but only in the codomain. One can never get back to the domain). This is useful in additive combinatorics.

Estimated changes

added structure add_freiman_hom
added theorem freiman_hom.coe_comp
added theorem freiman_hom.coe_mk
added theorem freiman_hom.comp_apply
added theorem freiman_hom.comp_assoc
added theorem freiman_hom.comp_id
added theorem freiman_hom.const_comp
added theorem freiman_hom.div_apply
added theorem freiman_hom.div_comp
added theorem freiman_hom.ext
added theorem freiman_hom.id_comp
added theorem freiman_hom.inv_apply
added theorem freiman_hom.inv_comp
added theorem freiman_hom.mk_coe
added theorem freiman_hom.mul_apply
added theorem freiman_hom.mul_comp
added theorem freiman_hom.one_apply
added theorem freiman_hom.one_comp
added structure freiman_hom
added theorem map_prod_eq_map_prod