Documentation

Mathlib.Algebra.Hom.Freiman

Freiman homomorphisms #

In this file, we define Freiman homomorphisms. A n-Freiman homomorphism on A is a function f : α → β→ β such that f (x₁) * ... * f (xₙ) = f (y₁) * ... * f (yₙ) for all x₁, ..., xₙ, y₁, ..., yₙ ∈ A∈ A such that x₁ * ... * xₙ = y₁ * ... * yₙ. In particular, any MulHom is a Freiman homomorphism.

They are of interest in additive combinatorics.

Main declaration #

Notation #

Implementation notes #

In the context of combinatorics, we are interested in Freiman homomorphisms over sets which are not necessarily closed under addition/multiplication. This means we must parametrize them with a set in an AddMonoid/Monoid instead of the AddMonoid/Monoid itself.

References #

Yufei Zhao, 18.225: Graph Theory and Additive Combinatorics

TODO #

MonoidHom.toFreimanHom could be relaxed to MulHom.toFreimanHom by proving (s.map f).prod = (t.map f).prod directly by induction instead of going through f s.prod.

Define n-Freiman isomorphisms.

Affine maps induce Freiman homs. Concretely, provide the AddFreimanHomClass (α →ₐ[𝕜] β) A β n→ₐ[𝕜] β) A β n instance.

structure AddFreimanHom {α : Type u_1} (A : Set α) (β : Type u_2) [inst : AddCommMonoid α] [inst : AddCommMonoid β] (n : ) :
Type (maxu_1u_2)

An additive n-Freiman homomorphism is a map which preserves sums of n elements.

Instances For
    structure FreimanHom {α : Type u_1} (A : Set α) (β : Type u_2) [inst : CommMonoid α] [inst : CommMonoid β] (n : ) :
    Type (maxu_1u_2)

    A n-Freiman homomorphism on a set A is a map which preserves products of n elements.

    Instances For

      An additive n-Freiman homomorphism is a map which preserves sums of n elements.

      Equations
      • One or more equations did not get rendered due to their size.

      A n-Freiman homomorphism on a set A is a map which preserves products of n elements.

      Equations
      • One or more equations did not get rendered due to their size.
      class AddFreimanHomClass {α : Type u_1} (F : Type u_2) (A : outParam (Set α)) (β : outParam (Type u_3)) [inst : AddCommMonoid α] [inst : AddCommMonoid β] (n : ) [inst : FunLike F α fun x => β] :

      AddFreimanHomClass F A β n states that F is a type of n-ary sums-preserving morphisms. You should extend this class when you extend AddFreimanHom.

      Instances
        class FreimanHomClass {α : Type u_1} (F : Type u_2) (A : outParam (Set α)) (β : outParam (Type u_3)) [inst : CommMonoid α] [inst : CommMonoid β] (n : ) [inst : FunLike F α fun x => β] :

        FreimanHomClass F A β n states that F is a type of n-ary products-preserving morphisms. You should extend this class when you extend FreimanHom.

        Instances
          def AddFreimanHomClass.toFreimanHom.proof_1 {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : FunLike F α fun x => β] [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } [inst : AddFreimanHomClass F A β n] (f : F) :
          ∀ {s t : Multiset α}, (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = nMultiset.card t = nMultiset.sum s = Multiset.sum tMultiset.sum (Multiset.map (f) s) = Multiset.sum (Multiset.map (f) t)
          Equations
          • One or more equations did not get rendered due to their size.
          def AddFreimanHomClass.toFreimanHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α fun x => β] [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } [inst : AddFreimanHomClass F A β n] (f : F) :
          A →+[n] β

          Turn an element of a type F satisfying AddFreimanHomClass F A β n into an actual AddFreimanHom. This is declared as the default coercion from F to AddFreimanHom A β n.

          Equations
          • One or more equations did not get rendered due to their size.
          def FreimanHomClass.toFreimanHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α fun x => β] [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } [inst : FreimanHomClass F A β n] (f : F) :
          A →*[n] β

          Turn an element of a type F satisfying FreimanHomClass F A β n into an actual FreimanHom. This is declared as the default coercion from F to FreimanHom A β n.

          Equations
          • One or more equations did not get rendered due to their size.
          instance instCoeTCFreimanHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α fun x => β] [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } [inst : FreimanHomClass F A β n] :
          CoeTC F (A →*[n] β)

          Any type satisfying SMulHomClass can be cast into MulActionHom via SMulHomClass.toMulActionHom.

          Equations
          • instCoeTCFreimanHom = { coe := FreimanHomClass.toFreimanHom }
          theorem map_sum_eq_map_sum {F : Type u_2} {α : Type u_1} {β : Type u_3} [inst : FunLike F α fun x => β] [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } [inst : AddFreimanHomClass F A β n] (f : F) {s : Multiset α} {t : Multiset α} (hsA : ∀ ⦃x : α⦄, x sx A) (htA : ∀ ⦃x : α⦄, x tx A) (hs : Multiset.card s = n) (ht : Multiset.card t = n) (h : Multiset.sum s = Multiset.sum t) :
          theorem map_prod_eq_map_prod {F : Type u_2} {α : Type u_1} {β : Type u_3} [inst : FunLike F α fun x => β] [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } [inst : FreimanHomClass F A β n] (f : F) {s : Multiset α} {t : Multiset α} (hsA : ∀ ⦃x : α⦄, x sx A) (htA : ∀ ⦃x : α⦄, x tx A) (hs : Multiset.card s = n) (ht : Multiset.card t = n) (h : Multiset.prod s = Multiset.prod t) :
          theorem map_add_map_eq_map_add_map {F : Type u_2} {α : Type u_1} {β : Type u_3} [inst : FunLike F α fun x => β] [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {a : α} {b : α} {c : α} {d : α} [inst : AddFreimanHomClass F A β 2] (f : F) (ha : a A) (hb : b A) (hc : c A) (hd : d A) (h : a + b = c + d) :
          f a + f b = f c + f d
          theorem map_mul_map_eq_map_mul_map {F : Type u_2} {α : Type u_1} {β : Type u_3} [inst : FunLike F α fun x => β] [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {a : α} {b : α} {c : α} {d : α} [inst : FreimanHomClass F A β 2] (f : F) (ha : a A) (hb : b A) (hc : c A) (hd : d A) (h : a * b = c * d) :
          f a * f b = f c * f d
          instance AddFreimanHom.funLike {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } :
          FunLike (A →+[n] β) α fun x => β
          Equations
          • AddFreimanHom.funLike = { coe := AddFreimanHom.toFun, coe_injective' := (_ : ∀ (f g : A →+[n] β), f.toFun = g.toFunf = g) }
          def AddFreimanHom.funLike.proof_1 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (f : A →+[n] β) (g : A →+[n] β) (h : f.toFun = g.toFun) :
          f = g
          Equations
          • (_ : f = g) = (_ : f = g)
          instance FreimanHom.funLike {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } :
          FunLike (A →*[n] β) α fun x => β
          Equations
          • FreimanHom.funLike = { coe := FreimanHom.toFun, coe_injective' := (_ : ∀ (f g : A →*[n] β), f.toFun = g.toFunf = g) }
          def AddFreimanHom.addFreimanHomClass.proof_1 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } :
          AddFreimanHomClass (A →+[n] β) A β n
          Equations
          instance FreimanHom.freimanHomClass {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } :
          FreimanHomClass (A →*[n] β) A β n
          Equations
          @[simp]
          theorem AddFreimanHom.toFun_eq_coe {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (f : A →+[n] β) :
          f.toFun = f
          @[simp]
          theorem FreimanHom.toFun_eq_coe {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } (f : A →*[n] β) :
          f.toFun = f
          theorem AddFreimanHom.ext {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } ⦃f : A →+[n] β ⦃g : A →+[n] β (h : ∀ (x : α), f x = g x) :
          f = g
          theorem FreimanHom.ext {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } ⦃f : A →*[n] β ⦃g : A →*[n] β (h : ∀ (x : α), f x = g x) :
          f = g
          @[simp]
          theorem AddFreimanHom.coe_mk {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (f : αβ) (h : ∀ (s t : Multiset α), (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = nMultiset.card t = nMultiset.sum s = Multiset.sum tMultiset.sum (Multiset.map f s) = Multiset.sum (Multiset.map f t)) :
          { toFun := f, map_sum_eq_map_sum' := fun {s t} => h s t } = f
          @[simp]
          theorem FreimanHom.coe_mk {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } (f : αβ) (h : ∀ (s t : Multiset α), (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = nMultiset.card t = nMultiset.prod s = Multiset.prod tMultiset.prod (Multiset.map f s) = Multiset.prod (Multiset.map f t)) :
          { toFun := f, map_prod_eq_map_prod' := fun {s t} => h s t } = f
          @[simp]
          theorem AddFreimanHom.mk_coe {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (f : A →+[n] β) (h : ∀ {s t : Multiset α}, (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = nMultiset.card t = nMultiset.sum s = Multiset.sum tMultiset.sum (Multiset.map (f) s) = Multiset.sum (Multiset.map (f) t)) :
          { toFun := f, map_sum_eq_map_sum' := h } = f
          @[simp]
          theorem FreimanHom.mk_coe {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } (f : A →*[n] β) (h : ∀ {s t : Multiset α}, (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = nMultiset.card t = nMultiset.prod s = Multiset.prod tMultiset.prod (Multiset.map (f) s) = Multiset.prod (Multiset.map (f) t)) :
          { toFun := f, map_prod_eq_map_prod' := h } = f
          def AddFreimanHom.id {α : Type u_1} [inst : AddCommMonoid α] (A : Set α) (n : ) :
          A →+[n] α

          The identity map from an additive commutative monoid to itself.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddFreimanHom.id.proof_1 {α : Type u_1} [inst : AddCommMonoid α] (A : Set α) (n : ) :
          ∀ {s t : Multiset α}, (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = nMultiset.card t = nMultiset.sum s = Multiset.sum tMultiset.sum (Multiset.map (fun x => x) s) = Multiset.sum (Multiset.map (fun x => x) t)
          Equations
          @[simp]
          theorem AddFreimanHom.id_apply {α : Type u_1} [inst : AddCommMonoid α] (A : Set α) (n : ) (x : α) :
          ↑(AddFreimanHom.id A n) x = x
          @[simp]
          theorem FreimanHom.id_apply {α : Type u_1} [inst : CommMonoid α] (A : Set α) (n : ) (x : α) :
          ↑(FreimanHom.id A n) x = x
          def FreimanHom.id {α : Type u_1} [inst : CommMonoid α] (A : Set α) (n : ) :
          A →*[n] α

          The identity map from a commutative monoid to itself.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddFreimanHom.comp.proof_1 {α : Type u_1} {β : Type u_3} {γ : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {A : Set α} {B : Set β} {n : } (f : B →+[n] γ) (g : A →+[n] β) (hAB : Set.MapsTo (g) A B) :
          ∀ {s t : Multiset α}, (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = nMultiset.card t = nMultiset.sum s = Multiset.sum tMultiset.sum (Multiset.map (f g) s) = Multiset.sum (Multiset.map (f g) t)
          Equations
          def AddFreimanHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {A : Set α} {B : Set β} {n : } (f : B →+[n] γ) (g : A →+[n] β) (hAB : Set.MapsTo (g) A B) :
          A →+[n] γ

          Composition of additive Freiman homomorphisms as an additive Freiman homomorphism.

          Equations
          • One or more equations did not get rendered due to their size.
          def FreimanHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst : CommMonoid β] [inst : CommMonoid γ] {A : Set α} {B : Set β} {n : } (f : B →*[n] γ) (g : A →*[n] β) (hAB : Set.MapsTo (g) A B) :
          A →*[n] γ

          Composition of Freiman homomorphisms as a Freiman homomorphism.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddFreimanHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {A : Set α} {B : Set β} {n : } (f : B →+[n] γ) (g : A →+[n] β) {hfg : Set.MapsTo (g) A B} :
          ↑(AddFreimanHom.comp f g hfg) = f g
          @[simp]
          theorem FreimanHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] [inst : CommMonoid γ] {A : Set α} {B : Set β} {n : } (f : B →*[n] γ) (g : A →*[n] β) {hfg : Set.MapsTo (g) A B} :
          ↑(FreimanHom.comp f g hfg) = f g
          theorem AddFreimanHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {A : Set α} {B : Set β} {n : } (f : B →+[n] γ) (g : A →+[n] β) {hfg : Set.MapsTo (g) A B} (x : α) :
          ↑(AddFreimanHom.comp f g hfg) x = f (g x)
          theorem FreimanHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] [inst : CommMonoid γ] {A : Set α} {B : Set β} {n : } (f : B →*[n] γ) (g : A →*[n] β) {hfg : Set.MapsTo (g) A B} (x : α) :
          ↑(FreimanHom.comp f g hfg) x = f (g x)
          theorem AddFreimanHom.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommMonoid γ] [inst : AddCommMonoid δ] {A : Set α} {B : Set β} {C : Set γ} {n : } (f : A →+[n] β) (g : B →+[n] γ) (h : C →+[n] δ) {hf : Set.MapsTo (f) A B} {hhg : Set.MapsTo (g) B C} {hgf : Set.MapsTo (f) A B} {hh : Set.MapsTo (↑(AddFreimanHom.comp g f hgf)) A C} :
          theorem FreimanHom.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : CommMonoid α] [inst : CommMonoid β] [inst : CommMonoid γ] [inst : CommMonoid δ] {A : Set α} {B : Set β} {C : Set γ} {n : } (f : A →*[n] β) (g : B →*[n] γ) (h : C →*[n] δ) {hf : Set.MapsTo (f) A B} {hhg : Set.MapsTo (g) B C} {hgf : Set.MapsTo (f) A B} {hh : Set.MapsTo (↑(FreimanHom.comp g f hgf)) A C} :
          theorem AddFreimanHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {A : Set α} {B : Set β} {n : } {g₁ : B →+[n] γ} {g₂ : B →+[n] γ} {f : A →+[n] β} (hf : Function.Surjective f) {hg₁ : Set.MapsTo (f) A B} {hg₂ : Set.MapsTo (f) A B} :
          AddFreimanHom.comp g₁ f hg₁ = AddFreimanHom.comp g₂ f hg₂ g₁ = g₂
          theorem FreimanHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] [inst : CommMonoid γ] {A : Set α} {B : Set β} {n : } {g₁ : B →*[n] γ} {g₂ : B →*[n] γ} {f : A →*[n] β} (hf : Function.Surjective f) {hg₁ : Set.MapsTo (f) A B} {hg₂ : Set.MapsTo (f) A B} :
          FreimanHom.comp g₁ f hg₁ = FreimanHom.comp g₂ f hg₂ g₁ = g₂
          theorem AddFreimanHom.cancel_right_on {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {A : Set α} {B : Set β} {n : } {g₁ : B →+[n] γ} {g₂ : B →+[n] γ} {f : A →+[n] β} (hf : Set.SurjOn (f) A B) {hf' : Set.MapsTo (f) A B} :
          Set.EqOn (↑(AddFreimanHom.comp g₁ f hf')) (↑(AddFreimanHom.comp g₂ f hf')) A Set.EqOn (g₁) (g₂) B
          theorem FreimanHom.cancel_right_on {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] [inst : CommMonoid γ] {A : Set α} {B : Set β} {n : } {g₁ : B →*[n] γ} {g₂ : B →*[n] γ} {f : A →*[n] β} (hf : Set.SurjOn (f) A B) {hf' : Set.MapsTo (f) A B} :
          Set.EqOn (↑(FreimanHom.comp g₁ f hf')) (↑(FreimanHom.comp g₂ f hf')) A Set.EqOn (g₁) (g₂) B
          theorem AddFreimanHom.cancel_left_on {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {A : Set α} {B : Set β} {n : } {g : B →+[n] γ} {f₁ : A →+[n] β} {f₂ : A →+[n] β} (hg : Set.InjOn (g) B) {hf₁ : Set.MapsTo (f₁) A B} {hf₂ : Set.MapsTo (f₂) A B} :
          Set.EqOn (↑(AddFreimanHom.comp g f₁ hf₁)) (↑(AddFreimanHom.comp g f₂ hf₂)) A Set.EqOn (f₁) (f₂) A
          theorem FreimanHom.cancel_left_on {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] [inst : CommMonoid γ] {A : Set α} {B : Set β} {n : } {g : B →*[n] γ} {f₁ : A →*[n] β} {f₂ : A →*[n] β} (hg : Set.InjOn (g) B) {hf₁ : Set.MapsTo (f₁) A B} {hf₂ : Set.MapsTo (f₂) A B} :
          Set.EqOn (↑(FreimanHom.comp g f₁ hf₁)) (↑(FreimanHom.comp g f₂ hf₂)) A Set.EqOn (f₁) (f₂) A
          @[simp]
          theorem AddFreimanHom.comp_id {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (f : A →+[n] β) {hf : Set.MapsTo (↑(AddFreimanHom.id A n)) A A} :
          @[simp]
          theorem FreimanHom.comp_id {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } (f : A →*[n] β) {hf : Set.MapsTo (↑(FreimanHom.id A n)) A A} :
          @[simp]
          theorem AddFreimanHom.id_comp {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {B : Set β} {n : } (f : A →+[n] β) {hf : Set.MapsTo (f) A B} :
          @[simp]
          theorem FreimanHom.id_comp {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {B : Set β} {n : } (f : A →*[n] β) {hf : Set.MapsTo (f) A B} :
          def AddFreimanHom.const {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] (A : Set α) (n : ) (b : β) :
          A →+[n] β

          AddFreimanHom.const An b is the Freiman homomorphism sending everything to b.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddFreimanHom.const.proof_1 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] (A : Set α) (n : ) (b : β) :
          ∀ {s t : Multiset α}, (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = nMultiset.card t = nMultiset.sum s = Multiset.sum tMultiset.sum (Multiset.map (fun x => b) s) = Multiset.sum (Multiset.map (fun x => b) t)
          Equations
          def FreimanHom.const {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] (A : Set α) (n : ) (b : β) :
          A →*[n] β

          FreimanHom.const A n b is the Freiman homomorphism sending everything to b.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddFreimanHom.const_apply {α : Type u_2} {β : Type u_1} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} (n : ) (b : β) (x : α) :
          ↑(AddFreimanHom.const A n b) x = b
          @[simp]
          theorem FreimanHom.const_apply {α : Type u_2} {β : Type u_1} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} (n : ) (b : β) (x : α) :
          ↑(FreimanHom.const A n b) x = b
          @[simp]
          theorem AddFreimanHom.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {A : Set α} {B : Set β} (n : ) (c : γ) (f : A →+[n] β) {hf : Set.MapsTo (f) A B} :
          @[simp]
          theorem FreimanHom.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst : CommMonoid β] [inst : CommMonoid γ] {A : Set α} {B : Set β} (n : ) (c : γ) (f : A →*[n] β) {hf : Set.MapsTo (f) A B} :
          instance AddFreimanHom.instZeroFreimanHom {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } :
          Zero (A →+[n] β)

          0 is the Freiman homomorphism sending everything to 0.

          Equations
          instance FreimanHom.instOneFreimanHom {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } :
          One (A →*[n] β)

          1 is the Freiman homomorphism sending everything to 1.

          Equations
          @[simp]
          theorem AddFreimanHom.zero_apply {α : Type u_2} {β : Type u_1} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (x : α) :
          0 x = 0
          @[simp]
          theorem FreimanHom.one_apply {α : Type u_2} {β : Type u_1} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } (x : α) :
          1 x = 1
          @[simp]
          theorem AddFreimanHom.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {A : Set α} {B : Set β} {n : } (f : A →+[n] β) {hf : Set.MapsTo (f) A B} :
          @[simp]
          theorem FreimanHom.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst : CommMonoid β] [inst : CommMonoid γ] {A : Set α} {B : Set β} {n : } (f : A →*[n] β) {hf : Set.MapsTo (f) A B} :
          instance AddFreimanHom.instInhabitedFreimanHom {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } :
          Equations
          • AddFreimanHom.instInhabitedFreimanHom = { default := 0 }
          instance FreimanHom.instInhabitedFreimanHom {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } :
          Equations
          • FreimanHom.instInhabitedFreimanHom = { default := 1 }
          def AddFreimanHom.instAddFreimanHom.proof_1 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (f : A →+[n] β) (g : A →+[n] β) :
          ∀ {s t : Multiset α}, (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = nMultiset.card t = nMultiset.sum s = Multiset.sum tMultiset.sum (Multiset.map (fun x => f x + g x) s) = Multiset.sum (Multiset.map (fun x => f x + g x) t)
          Equations
          • One or more equations did not get rendered due to their size.
          instance AddFreimanHom.instAddFreimanHom {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } :
          Add (A →+[n] β)

          f + g is the Freiman homomorphism sending x to f x + g x.

          Equations
          • One or more equations did not get rendered due to their size.
          instance FreimanHom.instMulFreimanHom {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } :
          Mul (A →*[n] β)

          f * g is the Freiman homomorphism sends x to f x * g x.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddFreimanHom.add_apply {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (f : A →+[n] β) (g : A →+[n] β) (x : α) :
          ↑(f + g) x = f x + g x
          @[simp]
          theorem FreimanHom.mul_apply {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } (f : A →*[n] β) (g : A →*[n] β) (x : α) :
          ↑(f * g) x = f x * g x
          theorem AddFreimanHom.add_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {A : Set α} {B : Set β} {n : } (g₁ : B →+[n] γ) (g₂ : B →+[n] γ) (f : A →+[n] β) {hg : Set.MapsTo (f) A B} {hg₁ : Set.MapsTo (f) A B} {hg₂ : Set.MapsTo (f) A B} :
          AddFreimanHom.comp (g₁ + g₂) f hg = AddFreimanHom.comp g₁ f hg₁ + AddFreimanHom.comp g₂ f hg₂
          theorem FreimanHom.mul_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] [inst : CommMonoid γ] {A : Set α} {B : Set β} {n : } (g₁ : B →*[n] γ) (g₂ : B →*[n] γ) (f : A →*[n] β) {hg : Set.MapsTo (f) A B} {hg₁ : Set.MapsTo (f) A B} {hg₂ : Set.MapsTo (f) A B} :
          FreimanHom.comp (g₁ * g₂) f hg = FreimanHom.comp g₁ f hg₁ * FreimanHom.comp g₂ f hg₂
          def AddFreimanHom.instNegFreimanHomToAddCommMonoid.proof_1 {α : Type u_1} {G : Type u_2} [inst : AddCommMonoid α] [inst : AddCommGroup G] {A : Set α} {n : } (f : A →+[n] G) :
          ∀ {s t : Multiset α}, (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = nMultiset.card t = nMultiset.sum s = Multiset.sum tMultiset.sum (Multiset.map (fun x => -f x) s) = Multiset.sum (Multiset.map (fun x => -f x) t)
          Equations
          • One or more equations did not get rendered due to their size.
          instance AddFreimanHom.instNegFreimanHomToAddCommMonoid {α : Type u_1} {G : Type u_2} [inst : AddCommMonoid α] [inst : AddCommGroup G] {A : Set α} {n : } :
          Neg (A →+[n] G)

          If f is a Freiman homomorphism to an additive commutative group, then -f is the Freiman homomorphism sending x to -f x.

          Equations
          • One or more equations did not get rendered due to their size.
          instance FreimanHom.instInvFreimanHomToCommMonoid {α : Type u_1} {G : Type u_2} [inst : CommMonoid α] [inst : CommGroup G] {A : Set α} {n : } :
          Inv (A →*[n] G)

          If f is a Freiman homomorphism to a commutative group, then f⁻¹⁻¹ is the Freiman homomorphism sending x to (f x)⁻¹⁻¹.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddFreimanHom.neg_apply {α : Type u_1} {G : Type u_2} [inst : AddCommMonoid α] [inst : AddCommGroup G] {A : Set α} {n : } (f : A →+[n] G) (x : α) :
          ↑(-f) x = -f x
          @[simp]
          theorem FreimanHom.inv_apply {α : Type u_1} {G : Type u_2} [inst : CommMonoid α] [inst : CommGroup G] {A : Set α} {n : } (f : A →*[n] G) (x : α) :
          f⁻¹ x = (f x)⁻¹
          @[simp]
          theorem AddFreimanHom.neg_comp {α : Type u_3} {β : Type u_1} {G : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommGroup G] {A : Set α} {B : Set β} {n : } (f : B →+[n] G) (g : A →+[n] β) {hf : Set.MapsTo (g) A B} {hf' : Set.MapsTo (g) A B} :
          @[simp]
          theorem FreimanHom.inv_comp {α : Type u_3} {β : Type u_1} {G : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] [inst : CommGroup G] {A : Set α} {B : Set β} {n : } (f : B →*[n] G) (g : A →*[n] β) {hf : Set.MapsTo (g) A B} {hf' : Set.MapsTo (g) A B} :
          def AddFreimanHom.instSubFreimanHomToAddCommMonoid.proof_1 {α : Type u_1} {G : Type u_2} [inst : AddCommMonoid α] [inst : AddCommGroup G] {A : Set α} {n : } (f : A →+[n] G) (g : A →+[n] G) :
          ∀ {s t : Multiset α}, (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = nMultiset.card t = nMultiset.sum s = Multiset.sum tMultiset.sum (Multiset.map (fun x => f x - g x) s) = Multiset.sum (Multiset.map (fun x => f x - g x) t)
          Equations
          • One or more equations did not get rendered due to their size.
          instance AddFreimanHom.instSubFreimanHomToAddCommMonoid {α : Type u_1} {G : Type u_2} [inst : AddCommMonoid α] [inst : AddCommGroup G] {A : Set α} {n : } :
          Sub (A →+[n] G)

          If f and g are additive Freiman homomorphisms to an additive commutative group, then f - g is the additive Freiman homomorphism sending x to f x - g x

          Equations
          • One or more equations did not get rendered due to their size.
          instance FreimanHom.instDivFreimanHomToCommMonoid {α : Type u_1} {G : Type u_2} [inst : CommMonoid α] [inst : CommGroup G] {A : Set α} {n : } :
          Div (A →*[n] G)

          If f and g are Freiman homomorphisms to a commutative group, then f / g is the Freiman homomorphism sending x to f x / g x.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddFreimanHom.sub_apply {α : Type u_1} {G : Type u_2} [inst : AddCommMonoid α] [inst : AddCommGroup G] {A : Set α} {n : } (f : A →+[n] G) (g : A →+[n] G) (x : α) :
          ↑(f - g) x = f x - g x
          @[simp]
          theorem FreimanHom.div_apply {α : Type u_1} {G : Type u_2} [inst : CommMonoid α] [inst : CommGroup G] {A : Set α} {n : } (f : A →*[n] G) (g : A →*[n] G) (x : α) :
          ↑(f / g) x = f x / g x
          @[simp]
          theorem AddFreimanHom.sub_comp {α : Type u_3} {β : Type u_1} {G : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] [inst : AddCommGroup G] {A : Set α} {B : Set β} {n : } (f₁ : B →+[n] G) (f₂ : B →+[n] G) (g : A →+[n] β) {hf : Set.MapsTo (g) A B} {hf₁ : Set.MapsTo (g) A B} {hf₂ : Set.MapsTo (g) A B} :
          AddFreimanHom.comp (f₁ - f₂) g hf = AddFreimanHom.comp f₁ g hf₁ - AddFreimanHom.comp f₂ g hf₂
          @[simp]
          theorem FreimanHom.div_comp {α : Type u_3} {β : Type u_1} {G : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] [inst : CommGroup G] {A : Set α} {B : Set β} {n : } (f₁ : B →*[n] G) (f₂ : B →*[n] G) (g : A →*[n] β) {hf : Set.MapsTo (g) A B} {hf₁ : Set.MapsTo (g) A B} {hf₂ : Set.MapsTo (g) A B} :
          FreimanHom.comp (f₁ / f₂) g hf = FreimanHom.comp f₁ g hf₁ / FreimanHom.comp f₂ g hf₂

          Instances #

          def AddFreimanHom.addCommMonoid.proof_3 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (a : A →+[n] β) :
          a + 0 = a
          Equations
          • (_ : a + 0 = a) = (_ : a + 0 = a)
          instance AddFreimanHom.addCommMonoid {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } :

          α →+[n] β→+[n] β is an AddCommMonoid.

          Equations
          def AddFreimanHom.addCommMonoid.proof_5 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } :
          ∀ (n : ) (x : A →+[n] β), nsmulRec (n + 1) x = nsmulRec (n + 1) x
          Equations
          • (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x) = (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x)
          def AddFreimanHom.addCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (a : A →+[n] β) (b : A →+[n] β) (c : A →+[n] β) :
          a + b + c = a + (b + c)
          Equations
          • (_ : a + b + c = a + (b + c)) = (_ : a + b + c = a + (b + c))
          def AddFreimanHom.addCommMonoid.proof_2 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (a : A →+[n] β) :
          0 + a = a
          Equations
          • (_ : 0 + a = a) = (_ : 0 + a = a)
          def AddFreimanHom.addCommMonoid.proof_6 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (a : A →+[n] β) (b : A →+[n] β) :
          a + b = b + a
          Equations
          • (_ : a + b = b + a) = (_ : a + b = b + a)
          def AddFreimanHom.addCommMonoid.proof_4 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } :
          ∀ (x : A →+[n] β), nsmulRec 0 x = nsmulRec 0 x
          Equations
          • (_ : nsmulRec 0 x = nsmulRec 0 x) = (_ : nsmulRec 0 x = nsmulRec 0 x)
          instance FreimanHom.commMonoid {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } :

          A →*[n] β→*[n] β is a CommMonoid.

          Equations
          def AddFreimanHom.addCommGroup.proof_3 {α : Type u_1} [inst : AddCommMonoid α] {A : Set α} {n : } {β : Type u_2} [inst : AddCommGroup β] :
          ∀ (n : ) (a : A →+[n] β), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a
          Equations
          def AddFreimanHom.addCommGroup.proof_1 {α : Type u_1} [inst : AddCommMonoid α] {A : Set α} {n : } {β : Type u_2} [inst : AddCommGroup β] :
          ∀ (a b : A →+[n] β), a - b = a + -b
          Equations
          def AddFreimanHom.addCommGroup.proof_6 {α : Type u_1} [inst : AddCommMonoid α] {A : Set α} {n : } {β : Type u_2} [inst : AddCommGroup β] (a : A →+[n] β) (b : A →+[n] β) :
          a + b = b + a
          Equations
          def AddFreimanHom.addCommGroup.proof_5 {α : Type u_1} [inst : AddCommMonoid α] {A : Set α} {n : } {β : Type u_2} [inst : AddCommGroup β] :
          ∀ (a : A →+[n] β), -a + a = 0
          Equations
          • (_ : -a + a = 0) = (_ : -a + a = 0)
          def AddFreimanHom.addCommGroup.proof_4 {α : Type u_1} [inst : AddCommMonoid α] {A : Set α} {n : } {β : Type u_2} [inst : AddCommGroup β] :
          ∀ (n : ) (a : A →+[n] β), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
          Equations
          def AddFreimanHom.addCommGroup.proof_2 {α : Type u_1} [inst : AddCommMonoid α] {A : Set α} {n : } {β : Type u_2} [inst : AddCommGroup β] :
          ∀ (a : A →+[n] β), zsmulRec 0 a = zsmulRec 0 a
          Equations
          • (_ : zsmulRec 0 a = zsmulRec 0 a) = (_ : zsmulRec 0 a = zsmulRec 0 a)
          instance AddFreimanHom.addCommGroup {α : Type u_1} [inst : AddCommMonoid α] {A : Set α} {n : } {β : Type u_2} [inst : AddCommGroup β] :

          If β is an additive commutative group, then A →*[n] β→*[n] β is an additive commutative group too.

          Equations
          • AddFreimanHom.addCommGroup = let src := AddFreimanHom.addCommMonoid; AddCommGroup.mk (_ : ∀ (a b : A →+[n] β), a + b = b + a)
          instance FreimanHom.commGroup {α : Type u_1} [inst : CommMonoid α] {A : Set α} {n : } {β : Type u_2} [inst : CommGroup β] :

          If β is a commutative group, then A →*[n] β→*[n] β is a commutative group too.

          Equations
          • FreimanHom.commGroup = let src := FreimanHom.commMonoid; CommGroup.mk (_ : ∀ (a b : A →*[n] β), a * b = b * a)

          Hom hierarchy #

          instance AddMonoidHom.addFreimanHomClass {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {n : } :
          AddFreimanHomClass (α →+ β) Set.univ β n

          An additive monoid homomorphism is naturally an AddFreimanHom on its entire domain.

          We can't leave the domain A : Set α of the AddFreimanHom a free variable, since it wouldn't be inferrable.

          Equations
          def AddMonoidHom.addFreimanHomClass.proof_1 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {n : } :
          AddFreimanHomClass (α →+ β) Set.univ β n
          Equations
          instance MonoidHom.freimanHomClass {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {n : } :
          FreimanHomClass (α →* β) Set.univ β n

          A monoid homomorphism is naturally a FreimanHom on its entire domain.

          We can't leave the domain A : Set α of the FreimanHom a free variable, since it wouldn't be inferrable.

          Equations
          def AddMonoidHom.toAddFreimanHom.proof_1 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] (A : Set α) (n : ) (f : α →+ β) :
          ∀ {s t : Multiset α}, (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = nMultiset.card t = nMultiset.sum s = Multiset.sum tMultiset.sum (Multiset.map (f) s) = Multiset.sum (Multiset.map (f) t)
          Equations
          • One or more equations did not get rendered due to their size.
          def AddMonoidHom.toAddFreimanHom {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] (A : Set α) (n : ) (f : α →+ β) :
          A →+[n] β

          An AddMonoidHom is naturally an AddFreimanHom

          Equations
          • One or more equations did not get rendered due to their size.
          def MonoidHom.toFreimanHom {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] (A : Set α) (n : ) (f : α →* β) :
          A →*[n] β

          A MonoidHom is naturally a FreimanHom.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddMonoidHom.toAddFreimanHom_coe {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCommMonoid β] {A : Set α} {n : } (f : α →+ β) :
          @[simp]
          theorem MonoidHom.toFreimanHom_coe {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } (f : α →* β) :
          ↑(MonoidHom.toFreimanHom A n f) = f
          theorem MonoidHom.toFreimanHom_injective {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CommMonoid β] {A : Set α} {n : } :
          theorem map_sum_eq_map_sum_of_le {F : Type u_2} {α : Type u_1} {β : Type u_3} [inst : FunLike F α fun x => β] [inst : AddCommMonoid α] [inst : AddCancelCommMonoid β] {A : Set α} {m : } {n : } [inst : AddFreimanHomClass F A β n] (f : F) {s : Multiset α} {t : Multiset α} (hsA : ∀ (x : α), x sx A) (htA : ∀ (x : α), x tx A) (hs : Multiset.card s = m) (ht : Multiset.card t = m) (hst : Multiset.sum s = Multiset.sum t) (h : m n) :
          theorem map_prod_eq_map_prod_of_le {F : Type u_2} {α : Type u_1} {β : Type u_3} [inst : FunLike F α fun x => β] [inst : CommMonoid α] [inst : CancelCommMonoid β] {A : Set α} {m : } {n : } [inst : FreimanHomClass F A β n] (f : F) {s : Multiset α} {t : Multiset α} (hsA : ∀ (x : α), x sx A) (htA : ∀ (x : α), x tx A) (hs : Multiset.card s = m) (ht : Multiset.card t = m) (hst : Multiset.prod s = Multiset.prod t) (h : m n) :
          def AddFreimanHom.toAddFreimanHom.proof_1 {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCancelCommMonoid β] {A : Set α} {m : } {n : } (h : m n) (f : A →+[n] β) :
          ∀ {s t : Multiset α}, (∀ ⦃x : α⦄, x sx A) → (∀ ⦃x : α⦄, x tx A) → Multiset.card s = mMultiset.card t = mMultiset.sum s = Multiset.sum tMultiset.sum (Multiset.map (f) s) = Multiset.sum (Multiset.map (f) t)
          Equations
          def AddFreimanHom.toAddFreimanHom {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCancelCommMonoid β] {A : Set α} {m : } {n : } (h : m n) (f : A →+[n] β) :
          A →+[m] β

          α →+[n] β→+[n] β is naturally included in α →+[m] β→+[m] β for any m ≤ n≤ n

          Equations
          • One or more equations did not get rendered due to their size.
          def FreimanHom.toFreimanHom {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CancelCommMonoid β] {A : Set α} {m : } {n : } (h : m n) (f : A →*[n] β) :
          A →*[m] β

          α →*[n] β→*[n] β is naturally included in A →*[m] β→*[m] β for any m ≤ n≤ n.

          Equations
          • One or more equations did not get rendered due to their size.
          theorem AddFreimanHom.addFreimanHomClass_of_le {F : Type u_2} {α : Type u_1} {β : Type u_3} [inst : FunLike F α fun x => β] [inst : AddCommMonoid α] [inst : AddCancelCommMonoid β] {A : Set α} {m : } {n : } [inst : AddFreimanHomClass F A β n] (h : m n) :

          An additive n-Freiman homomorphism is also an additive m-Freiman homomorphism for any m ≤ n≤ n.

          theorem FreimanHom.FreimanHomClass_of_le {F : Type u_2} {α : Type u_1} {β : Type u_3} [inst : FunLike F α fun x => β] [inst : CommMonoid α] [inst : CancelCommMonoid β] {A : Set α} {m : } {n : } [inst : FreimanHomClass F A β n] (h : m n) :

          A n-Freiman homomorphism is also a m-Freiman homomorphism for any m ≤ n≤ n.

          @[simp]
          theorem AddFreimanHom.toAddFreimanHom_coe {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCancelCommMonoid β] {A : Set α} {m : } {n : } (h : m n) (f : A →+[n] β) :
          @[simp]
          theorem FreimanHom.toFreimanHom_coe {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CancelCommMonoid β] {A : Set α} {m : } {n : } (h : m n) (f : A →*[n] β) :
          theorem AddFreimanHom.toAddFreimanHom_injective {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst : AddCancelCommMonoid β] {A : Set α} {m : } {n : } (h : m n) :
          theorem FreimanHom.toFreimanHom_injective {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst : CancelCommMonoid β] {A : Set α} {m : } {n : } (h : m n) :