AddFreimanHom.map_sum_eq_map_sum'
theorem AddFreimanHom.map_sum_eq_map_sum' :
∀ {α : Type u_2} {A : Set α} {β : Type u_7} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {n : ℕ}
(self : A →+[n] β) {s t : Multiset α},
(∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
(∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
Multiset.card s = n →
Multiset.card t = n → s.sum = t.sum → (Multiset.map self.toFun s).sum = (Multiset.map self.toFun t).sum
This theorem, `AddFreimanHom.map_sum_eq_map_sum'`, states that for any given types `α` and `β`, a set `A` of type `α`, two multisets `s` and `t` of type `α`, and a natural number `n`, given that `α` and `β` are both additive commutative monoids and there exists an `n`-Freiman homomorphism from set `A` to `β`, if every element of `s` and `t` belongs to the set `A`, and if `s` and `t` have the same cardinality `n` and their sums are equal, then the sum of the image of `s` under the homomorphism equals the sum of the image of `t` under the homomorphism. In other words, an `n`-Freiman homomorphism preserves the sum of `n` elements.
More concisely: Given sets `A` of type `α`, `β`, multisets `s` and `t` of type `α`, and a natural number `n`, if `α` and `β` are additive commutative monoids, `A` has an `n`-Freiman homomorphism, and every element of `s` and `t` is in `A`, with `s`, `t`, and their sums having the same cardinality `n`, then the sum of the images of `s` and `t` under the homomorphism are equal.
|
AddFreimanHom.addFreimanHomClass_of_le
theorem AddFreimanHom.addFreimanHomClass_of_le :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddCommMonoid α]
[inst_2 : AddCancelCommMonoid β] {A : Set α} {m n : ℕ} [inst_3 : AddFreimanHomClass F A β n],
m ≤ n → AddFreimanHomClass F A β m
This theorem, termed `AddFreimanHom.addFreimanHomClass_of_le`, states that for any types `F`, `α`, and `β`, given that `F` is a function-like structure from `α` to `β`, `α` is an additive commutative monoid, and `β` is an additive cancellative commutative monoid. If `A` is a set of `α` and for any natural numbers `m` and `n`, if `F` is an additive `n`-Freiman homomorphism on `A` in `β`, then if `m` is less than or equal to `n`, `F` is also an additive `m`-Freiman homomorphism on `A` in `β`.
In simpler terms, if a function-like structure preserves the additive structure of `n` elements from a set in an additive commutative monoid to an additive cancellative commutative monoid, it will also preserve the additive structure of `m` elements if `m` is less than or equal to `n`. This is a property of additive Freiman homomorphisms.
More concisely: If `F` is an additive `n`-Freiman homomorphism from an additive commutative monoid `α` to an additive cancellative commutative monoid `β`, then `F` is also an additive `m`-Freiman homomorphism for any `m ≤ n`.
|
FreimanHom.ext
theorem FreimanHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {n : ℕ} ⦃f g : A →*[n] β⦄,
(∀ (x : α), f x = g x) → f = g
This theorem, referred to as `FreimanHom.ext`, states that for any two types `α` and `β` with the structures of commutative monoids, for a set `A` of elements of type `α` and any natural number `n`, if `f` and `g` are Freiman homomorphisms from `A` to `β` of order `n`, and if `f` and `g` map every element `x` of the set `A` to the same element in `β`, then `f` and `g` are indeed the same Freiman homomorphism. In other words, it ensures the uniqueness of a Freiman homomorphism under the described conditions.
More concisely: If `α` and `β` are commutative monoids, `A` is a set of elements from `α`, `n` is a natural number, `f` and `g` are Freiman homomorphisms from `A` to `β` of order `n`, and `f(x) = g(x)` for all `x ∈ A`, then `f = g`.
|
FreimanHomClass.map_prod_eq_map_prod'
theorem FreimanHomClass.map_prod_eq_map_prod' :
∀ {α : Type u_2} {F : Type u_7} {A : outParam (Set α)} {β : outParam (Type u_8)} [inst : CommMonoid α]
[inst_1 : CommMonoid β] {n : ℕ} [inst_2 : FunLike F α β] [self : FreimanHomClass F A β n] (f : F)
{s t : Multiset α},
(∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
(∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
Multiset.card s = n →
Multiset.card t = n → s.prod = t.prod → (Multiset.map (⇑f) s).prod = (Multiset.map (⇑f) t).prod
This theorem, `FreimanHomClass.map_prod_eq_map_prod'`, states that for any two multisets `s` and `t` of type `α`, a type with a commutative monoid structure, and a function `f` which is a `n`-Freiman homomorphism from a set `A` of type `α` to a type `β` with a commutative monoid structure, if all elements of `s` and `t` are in `A`, and if `s` and `t` have the same cardinality `n`, and their products are equal, then the products of the images of `s` and `t` under `f` are also equal.
In terms of sets, this theorem says that if we have two equal-sized sets of numbers where the product of numbers in each set is the same, and if we have a function that preserves the structure of the set in some way, then the product of the transformed elements of each set will also be the same. This function, in particular, is an `n`-Freiman homomorphism which is a function that preserves certain properties of the set when we look at `n` elements at a time.
More concisely: Given two multisets of size `n` over a commutative monoid `α` with all elements in a set `A`, if their products are equal and `f` is an `n`-Freiman homomorphism from `A` to a commutative monoid `β`, then the products of the images of the multisets under `f` are equal.
|
AddFreimanHom.ext
theorem AddFreimanHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {n : ℕ}
⦃f g : A →+[n] β⦄, (∀ (x : α), f x = g x) → f = g
This theorem, `AddFreimanHom.ext`, states that for any two Additive Freiman homomorphisms `f` and `g` from a set `A` of a certain type `α` (with `α` being an additive commutative monoid) to another type `β` (also an additive commutative monoid), if `f` and `g` are equal for every element `x` in `α`, then the two homomorphisms `f` and `g` are themselves identical. An Additive Freiman homomorphism here is a function that preserves the additive structure under a certain condition related to the natural number `n`.
More concisely: If `f` and `g` are Additive Freiman homomorphisms from an additive commutative monoid `α` to another additive commutative monoid `β`, and `f(x) = g(x)` for all `x` in `α`, then `f = g`.
|
FreimanHom.FreimanHomClass_of_le
theorem FreimanHom.FreimanHomClass_of_le :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : CommMonoid α]
[inst_2 : CancelCommMonoid β] {A : Set α} {m n : ℕ} [inst_3 : FreimanHomClass F A β n],
m ≤ n → FreimanHomClass F A β m
The theorem `FreimanHom.FreimanHomClass_of_le` states that for any types `F`, `α`, and `β` where `F` is function-like from `α` to `β`, and for any commutative monoid on `α` and any cancelable commutative monoid on `β`, given a set `A` of `α` and any natural numbers `m` and `n`, if `F` is an `n`-Freiman homomorphism (a type of function that preserves certain properties of the set `A` under multiplication) then `F` is also a `m`-Freiman homomorphism for any `m` that is less than or equal to `n`.
In simple words, if a function is an `n`-Freiman homomorphism, it will also be a `m`-Freiman homomorphism for all `m` less than or equal to `n`.
More concisely: If `F : α -> β` is an `n`-Freiman homomorphism over commutative monoids on `α` and `β`, then `F` is also an `m`-Freiman homomorphism for all `m <= n`.
|
AddFreimanHomClass.map_sum_eq_map_sum'
theorem AddFreimanHomClass.map_sum_eq_map_sum' :
∀ {α : Type u_2} {F : Type u_7} {A : outParam (Set α)} {β : outParam (Type u_8)} [inst : AddCommMonoid α]
[inst_1 : AddCommMonoid β] {n : ℕ} [inst_2 : FunLike F α β] [self : AddFreimanHomClass F A β n] (f : F)
{s t : Multiset α},
(∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
(∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
Multiset.card s = n →
Multiset.card t = n → s.sum = t.sum → (Multiset.map (⇑f) s).sum = (Multiset.map (⇑f) t).sum
This theorem states that in a context with two commutative add monoids, `α` and `β`, a set `A` within `α`, a natural number `n`, and a function `F` that behaves like a function from `α` to `β`, if you have an additive `n`-Freiman homomorphism `f` from `F`, then for any two multisets `s` and `t` of `α` such that every element of `s` and `t` belongs to `A`, and both `s` and `t` have cardinality `n` and their sums are equal, the sums of the multisets obtained by mapping `s` and `t` with `f` will also be equal.
A Freiman homomorphism of order `n` is a function that preserves sums of `n` elements, and an additive Freiman homomorphism specifically operates within the context of additive commutative monoids. A multiset is a generalization of the concept of a set that allows for multiple instances of the elements.
More concisely: Given commutative add monoids `α` and `β`, a set `A` within `α`, a natural number `n`, a function `F` from `α` to `β`, an additive `n`-Freiman homomorphism `f` from `F`, and two multisets `s` and `t` of `A` with cardinality `n` and equal sums, the images of `s` and `t` under `f` have equal sums.
|
FreimanHom.map_prod_eq_map_prod'
theorem FreimanHom.map_prod_eq_map_prod' :
∀ {α : Type u_2} {A : Set α} {β : Type u_7} [inst : CommMonoid α] [inst_1 : CommMonoid β] {n : ℕ} (self : A →*[n] β)
{s t : Multiset α},
(∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
(∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
Multiset.card s = n →
Multiset.card t = n →
s.prod = t.prod → (Multiset.map self.toFun s).prod = (Multiset.map self.toFun t).prod
The theorem `FreimanHom.map_prod_eq_map_prod'` states that for any two multisets `s` and `t` of a type `α`, under conditions where `α` and `β` are both commutative monoids, and all elements of `s` and `t` belong to a set `A`, an `n`-Freiman homomorphism (represented as `self`) preserves the products of `n` elements. This means that if the cardinalities of both `s` and `t` are `n`, and the product of the elements in `s` is equal to the product of the elements in `t`, then the product of the `n` elements mapped from `s` to `β` via the Freiman homomorphism is equal to the product of the `n` elements mapped from `t` to `β`. This is significant in the study of additive number theory, as Freiman's theorem is a central result in this area.
More concisely: Given multisets `s` and `t` of commutative monoid type `α` with all elements in a set `A`, and an `n`-Freiman homomorphism `self` from `α` to `β`, if the products of `n` elements in `s` and `t` are equal, then the products of the images of these `n` elements under `self` are equal.
|
map_sum_eq_map_sum
theorem map_sum_eq_map_sum :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddCommMonoid α]
[inst_2 : AddCommMonoid β] {A : Set α} {n : ℕ} [inst_3 : AddFreimanHomClass F A β n] (f : F) {s t : Multiset α},
(∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
(∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
Multiset.card s = n →
Multiset.card t = n → s.sum = t.sum → (Multiset.map (⇑f) s).sum = (Multiset.map (⇑f) t).sum
The theorem `map_sum_eq_map_sum` states that for any type `F` with a function-like structure from `α` to `β`, and any commutative additive monoid structures on `α` and `β`, given a set `A` of `α`, a natural number `n`, and an `AddFreimanHomClass` instance from `F A β n`, if we have a function `f` of type `F` and two multisets `s` and `t` of type `α` such that all elements of `s` and `t` belong to `A`, and both `s` and `t` have a cardinality of `n`, then if the sum of elements in `s` is equal to the sum of elements in `t`, it follows that the sum of elements in the mapped multisets `map f s` and `map f t` are also equal. In terms of mathematical functions, if for two finite multisets `s` and `t` with same sum and cardinality, each element belongs to a set `A`, then the sum of the image of `s` under any function `f` from a function-like structure `F` is equal to the sum of the image of `t` under the same function.
More concisely: Given a commutative additive monoid with an AddFreimanHomClass instance, if two finite multisets of an element set have equal sum and belong to the set, then the images of these multisets under any function-like structure's function have equal sums.
|
map_prod_eq_map_prod
theorem map_prod_eq_map_prod :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : CommMonoid α]
[inst_2 : CommMonoid β] {A : Set α} {n : ℕ} [inst_3 : FreimanHomClass F A β n] (f : F) {s t : Multiset α},
(∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
(∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
Multiset.card s = n →
Multiset.card t = n → s.prod = t.prod → (Multiset.map (⇑f) s).prod = (Multiset.map (⇑f) t).prod
The theorem `map_prod_eq_map_prod` states that for any types `F`, `α`, and `β`, given a function-like `F` from `α` to `β`, commutative monoid structures on `α` and `β`, a set `A` of elements of type `α`, an integer `n`, and a Freiman homomorphism from `A` to `β` of size `n`. If there are two multisets `s` and `t` of type `α` such that every element in `s` and `t` belongs to `A`, both `s` and `t` have a cardinality of `n`, and the product of elements in `s` and `t` are equal, then the product of the mapped elements of `s` and `t` under function `f` are also equal. Here, "mapped elements" refers to the elements obtained by applying the function `f` to each element in the respective multisets.
In mathematical terms, if two multisets `s` and `t` have the same cardinality and their products are equal, then the product of their images under a Freiman homomorphism `f` is also equal.
More concisely: Given commutative monoids `α` and `β`, a function-like `F : α → β`, a set `A ⊆ α` with a Freiman homomorphism of size `n : ℕ`, and multisets `s` and `t` of `A` with equal cardinality `n` and product `∏s = ∏t`, then `∏(F <$> s) = ∏(F <$> t)`.
|