Finsupp.sum_apply
theorem Finsupp.sum_apply :
∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N]
{f : α →₀ M} {g : α → M → β →₀ N} {a₂ : β}, (f.sum g) a₂ = f.sum fun a₁ b => (g a₁ b) a₂
The theorem `Finsupp.sum_apply` states that for all types `α`, `β`, `M`, `N`, where `M` is equipped with a zero and `N` is an additive commutative monoid, given a function `f` from `α` to `M` with finite support, a function `g` from `α` and `M` to `β` with finite support, and an element `a₂` of type `β`, the application of the sum of `g a (f a)` over the support of `f` to `a₂` is equal to the sum over the support of `f` of the function that maps `a₁` and `b` to the application of `g a₁ b` to `a₂`. In mathematical notation, it means that $\sum_{a\in \text{supp}(f)} (g(a, f(a))(a_2)) = \sum_{a\in \text{supp}(f)} g(a, f(a))(a_2)$ for all `a₂` in `β`.
More concisely: For all types `α`, `β`, `M` (an additive commutative monoid), given functions `f: α → M` and `g: α × M → β` with finite support, and `a₂ ∈ β`, we have $\sum\_{a \in \text{supp}(f)} g(a, f(a))(a\_2) = \sum\_{a \in \text{supp}(f)} g(a, f(a))(a)$.
|
Finsupp.add_sum_erase'
theorem Finsupp.add_sum_erase' :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] (f : α →₀ M) (y : α)
(g : α → M → N), (∀ (i : α), g i 0 = 0) → g y (f y) + (Finsupp.erase y f).sum g = f.sum g
This theorem, named `Finsupp.add_sum_erase'`, generalizes the `Finsupp.add_sum_erase` property. It states that for any finitely supported function `f` from a type `α` to a type `M` with zero, any element `y` of type `α`, and any function `g` from `α` and `M` to a type `N`, if `g` maps a second argument of zero to zero, then the sum of `g` over `f` is equal to the sum of the function `g` applied to `y` and the value of `f` at `y`, added to the sum of `g` over the function obtained from `f` by erasing the value at `y`. In mathematical terms, it means that $\sum_{i \in \text{supp}(f)} g(i, f(i)) = g(y, f(y)) + \sum_{i \in \text{supp}(f) \setminus \{y\}} g(i, f(i))$, assuming that $g(i, 0) = 0$ for all $i$.
More concisely: Given a finitely supported function `f` from type `α` to type `M` with zero, and a function `g` from `α` and `M` to type `N` satisfying `g(i, 0) = 0` for all `i`, then $\sum_{i \in \text{supp}(f)} g(i, f(i)) = g(y, f(y)) + \sum_{i \in \text{supp}(f) \setminus \{y\}} g(i, f(i))$ for any `y` in `α`.
|
Finsupp.prod_single_index
theorem Finsupp.prod_single_index :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {a : α} {b : M}
{h : α → M → N}, h a 0 = 1 → (fun₀ | a => b).prod h = h a b
The theorem `Finsupp.prod_single_index` states that for all types `α`, `M`, `N` where `M` has a zero instance and `N` a commutative monoid instance, and for any element `a` of type `α`, any element `b` of type `M`, and any function `h` from `α` and `M` to `N`, if `h a 0` is equal to 1, then the product of `h a (f a)` over the support of `f`, where `f` is a function from `α` to `M` defined as `f(a) = b` and `f(x) = 0` for `x ≠ a`, is equal to `h a b`. This means that in this specific case, the product is not affected by the other zero values of the function.
More concisely: For any commutative monoid `N`, function `h : α × M → N`, and element `a : α` with `M` having a zero, if `h(a, 0) = 1`, then the product of `h(a, b)` over the support of the function `f : α → M` defined as `f(x) = b` for `x = a` and `0` otherwise, equals `h(a, b)`.
|
Finsupp.sum_mapRange_index
theorem Finsupp.sum_mapRange_index :
∀ {α : Type u_1} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [inst : Zero M] [inst_1 : Zero M']
[inst_2 : AddCommMonoid N] {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h : α → M' → N},
(∀ (a : α), h a 0 = 0) → (Finsupp.mapRange f hf g).sum h = g.sum fun a b => h a (f b)
The theorem `Finsupp.sum_mapRange_index` states that for any types `α`, `M`, `M'`, `N`, where `M`, `M'` are equipped with a zero and `N` is an additive commutative monoid, given a function `f : M → M'` that maps zero to zero, a function `g : α →₀ M` (a finite support function from `α` to `M`), a function `h : α → M' → N` and the condition that `h a 0 = 0` for all `a` in `α`, the sum over the support of `g` mapped through `f` using function `h` is equal to the sum over the support of `g` using `h` applied to `a` and `f(b)`. Here, the sum is computed as the sum of `h a (f a)` over the support of `f` (which is a finite set of values away from which `f` is zero).
More concisely: For functions `f : M -> M'` mapping zero to zero, `g : α ->0 M`, and `h : α -> M' -> N` with `h a 0 = 0` for all `a`, the sum of `h a (f a)` over the support of `g` is equal to the sum of `h a b` over the support of `g` for all `b` in the support of `g`.
|
Finsupp.mul_prod_erase'
theorem Finsupp.mul_prod_erase' :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] (f : α →₀ M) (y : α)
(g : α → M → N), (∀ (i : α), g i 0 = 1) → g y (f y) * (Finsupp.erase y f).prod g = f.prod g
This theorem generalizes the `Finsupp.mul_prod_erase` theorem and states that if a function `g` assigns a value of 1 to any second argument of 0, then the product of `g` over a finitely supported function `f : α →₀ M` is the same as the product of multiplying the value on any element `y : α` by the product over `f` with `y` erased. In other words, summing over all elements of `f` with the function `g` is equivalent to multiplying the value of `g` at `y` with the sum over the remaining elements of `f` after erasing `y`. The theorem holds for any `α`, `M` and `N`, where `M` is a type with zero and `N` is a type with a commutative multiplication operation.
More concisely: If `g` is a function that maps arguments to 1 when the second argument is 0, then the product of `g` and a finitely supported function `f` is equal to multiplying the value of `g` at any `y` by the product of `f` with `y` erased.
|
Finsupp.sum_single_index
theorem Finsupp.sum_single_index :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {a : α} {b : M}
{h : α → M → N}, h a 0 = 0 → (fun₀ | a => b).sum h = h a b
The theorem `Finsupp.sum_single_index` states that for all types α, M and N, where M is equipped with a Zero structure and N has an Additive Commutative Monoid structure, for any elements 'a' of type α and 'b' of type M, and a function 'h' from pairs of type α and M to N, if applying 'h' to 'a' and 0 yields 0, then the sum (using the `Finsupp.sum` definition) of the function 'h' applied to elements of the support of the singleton function (which maps 'a' to 'b' and everything else to 0) is equal to the result of applying 'h' to 'a' and 'b'. In simpler terms, this theorem relates the sum over a singleton set to a direct application of the function in question.
More concisely: For any type α, M with Zero structure, and N with Additive Commutative Monoid structure, if the function h from α × M to N satisfies h(a, 0) = 0 for all a ∈ α, then Σ(x : α) h(x, m) = h(a, m) for any singleton function {a} → M mapping to m.
|
Finsupp.sum_single
theorem Finsupp.sum_single :
∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] (f : α →₀ M), f.sum Finsupp.single = f
The theorem `Finsupp.sum_single` is about finite support functions in Lean. It states that for any type `α` and any type `M` which is an additive commutative monoid, given a function `f` from `α` to `M` with finite support, the sum of the function `Finsupp.single` over the support of `f` is equal to `f` itself. Therefore, this theorem reveals a kind of 'self-reversibility' of the `Finsupp.single` function under the `Finsupp.sum` operation.
More concisely: For any additive commutative monoid type `M` and type `α` with finite support function `f` from `α` to `M`, `Finsupp.sum (Finsupp.single x hx : Finsupp α M) = f x` for all `x : α` in the support of `f`.
|
Finsupp.add_sum_erase
theorem Finsupp.add_sum_erase :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] (f : α →₀ M) (y : α)
(g : α → M → N), y ∈ f.support → g y (f y) + (Finsupp.erase y f).sum g = f.sum g
The theorem `Finsupp.add_sum_erase` states that for any finitely supported function `f : α →₀ M` over some type `α` with values in a type `M`, a function `g : α → M → N`, and a specific element `y : α` in the support of `f`, the sum of the function `g` evaluated over `f` is equal to the sum of `g` evaluated over the function obtained by erasing `y` from `f` (`Finsupp.erase y f`), plus `g` evaluated at `y` on `f`. This essentially means that we can isolate the contribution of a single element to the overall sum by first erasing it from the function and adding it back separately. The erasure operation sets the value of the function at `y` to 0.
More concisely: For any finitely supported function `f : α →₀ M`, element `y : α` in the support of `f`, and function `g : α → M → N`, we have `∑ (x : α), g x (f x) = g y (f y) + ∑ (x : α \{y}), g x (Finsupp.erase y f)`.
|
Finsupp.sum_zero_index
theorem Finsupp.sum_zero_index :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {h : α → M → N},
Finsupp.sum 0 h = 0
The theorem `Finsupp.sum_zero_index` states that for any types `α`, `M`, and `N` where `M` has an instance of `Zero` and `N` is an additive commutative monoid, and any function `h` from `α` and `M` to `N`, the sum of `h a (f a)` over the support of the zero function (`f = 0`) is zero. This is equivalent to stating that the sum of the function `h` over an empty set of inputs (since the support of the zero function is empty) is zero.
More concisely: For any additive commutative monoid N with zero element, function h from type α x M to N, and zero function f on α, the sum of h (a, x) over the support of f (where a is an element of α) is zero.
|
Finsupp.sum_fintype
theorem Finsupp.sum_fintype :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] [inst_2 : Fintype α]
(f : α →₀ M) (g : α → M → N), (∀ (i : α), g i 0 = 0) → f.sum g = Finset.univ.sum fun i => g i (f i)
The theorem `Finsupp.sum_fintype` states that for any types `α`, `M`, and `N`, given `M` is a type with a zero element and `N` is a type forming an additive commutative monoid, and `α` is a finite type. If we have a function `f` from `α` to `M` and a function `g` from `α` and `M` to `N` such that `g i 0 = 0` for all `i` in `α`, then the sum of `g a (f a)` over the support of `f` is equal to the sum of `g i (f i)` for every element `i` in the universal finite set of type `α`. This sum is defined in terms of `Finset.sum`, which sums a function over elements of a finite set, and `Finsupp.sum`, which sums a function over the support of another function.
More concisely: For any finite type `α`, functions `f : α → M` and `g : α × M → N` with `M` an additive commutative monoid and `g(i, 0) = 0` for all `i` in `α`, the sum of `g(i, f(i))` over `α` equals the sum of `g(i, f(i))` over the support of `f` according to `Finset.sum` and `Finsupp.sum`.
|
Finsupp.prod_add_index'
theorem Finsupp.prod_add_index' :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : CommMonoid N] {f g : α →₀ M}
{h : α → M → N},
(∀ (a : α), h a 0 = 1) →
(∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) → (f + g).prod h = f.prod h * g.prod h
This theorem states that when taking the product under a function `h` across the elements of two finitely supported functions `f` and `g`, it respects the operation of addition, behaving like a homomorphism from additive to multiplicative domains, provided `h` itself is an additive-to-multiplicative homomorphism. In other words, for any finitely supported functions `f` and `g` with elements of type `M` and a function `h` that maps elements of type `α` and `M` to `N`, if `h` maps each `a` to `1` when paired with zero and satisfies the property that `h(a, b₁ + b₂)` equals `h(a, b₁) * h(a, b₂)` for any `b₁` and `b₂`, then the product of `h` over `f + g` equals the product of `f` and `g` under `h`. This is a more specialized version of `Finsupp.prod_add_index` with simpler hypotheses.
More concisely: Given finitely supported functions `f` and `g` with additive domain `M` and a function `h: α × M → N` that is an additive-to-multiplicative homomorphism, the product of `h` over the sum of `f` and `g` equals the product of `h` over `f` and `g`.
|
RingHom.map_finsupp_sum
theorem RingHom.map_finsupp_sum :
∀ {α : Type u_1} {M : Type u_8} {R : Type u_14} {S : Type u_15} [inst : Zero M] [inst_1 : Semiring R]
[inst_2 : Semiring S] (h : R →+* S) (f : α →₀ M) (g : α → M → R), h (f.sum g) = f.sum fun a b => h (g a b)
The theorem `RingHom.map_finsupp_sum` states that for any types `α`, `M`, `R` and `S` where `M` is a type with a zero element, `R` and `S` are semirings, `f` is a finitely supported function from `α` to `M`, `g` is a function from `α` and `M` to `R`, and `h` is a ring homomorphism from `R` to `S`, the result of mapping the sum of the result of `g` applied to the elements of `f` through `h` is the same as the sum of the result of `h` applied to `g` for each element in `f`. In mathematical terms, this can be represented as $$h \left(\sum_{a \in f} g(a)\right) = \sum_{a \in f} h(g(a)).$$ However, this theorem is deprecated and it is recommended to use `_root_.map_finsupp_sum` instead.
More concisely: Given a semiring homomorphism `h` from `R` to `S`, a semiring `R`, a zeroed type `M`, a finitely supported function `f` from `α` to `M`, and functions `g: α × M → R`, the application of `h` to the sum of `g` applied to each element in `f` equals the sum of applying `h` to each `g(a, x)` for `a ∈ α` and `x ∈ f(a)`. In other words, `h (∑(a ∈ α) g(a, f(a))) = ∑(a ∈ α) h(g(a, f(a)))`.
|
map_finsupp_prod
theorem map_finsupp_prod :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [inst : Zero M] [inst_1 : CommMonoid N]
[inst_2 : CommMonoid P] {H : Type u_16} [inst_3 : FunLike H N P] [inst_4 : MonoidHomClass H N P] (h : H)
(f : α →₀ M) (g : α → M → N), h (f.prod g) = f.prod fun a b => h (g a b)
The theorem `map_finsupp_prod` states that for all types `α`, `M`, `N`, `P`, and `H`, where `M` has a zero element, `N` and `P` are commutative monoids, `H` is a function-like structure from `N` to `P`, and `H` is a monoid homomorphism class from `N` to `P`, then for any such function `h`, function `f` from `α` to `M` with finite support, and function `g` from `α` and `M` to `N`, applying `h` to the product of `g a (f a)` over the support of `f` is equivalent to taking this product with `h (g a b)`. In mathematical terms, it says that $h \big(\prod_{a \in \mathrm{supp}(f)} g(a, f(a))\big) = \prod_{a \in \mathrm{supp}(f)} h(g(a, b))$. This theorem is primarily about the ability to interchange a monoid homomorphism with the operation of taking a product over the support of a function.
More concisely: For functions `h` from a commutative monoid `N` to another commutative monoid `P` that is a monoid homomorphism, and given functions `f : α → M` with finite support and `g : α → M → N`, the product of `h (g a b)` over `α` is equal to `h (∏_{a ∈ supp(f)} g a (f a))`.
|
AddEquiv.map_finsupp_sum
theorem AddEquiv.map_finsupp_sum :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [inst : Zero M] [inst_1 : AddCommMonoid N]
[inst_2 : AddCommMonoid P] (h : N ≃+ P) (f : α →₀ M) (g : α → M → N), h (f.sum g) = f.sum fun a b => h (g a b)
This theorem states that for any types `α`, `M`, `N`, and `P`, where `M` is a type with zero and `N` and `P` are types with additive commutative monoid structures, and for any additive equivalence `h` between `N` and `P`, any finitely supported function `f` from `α` to `M`, and any function `g` from `α` and `M` to `N`, the result of applying `h` to the sum (over the support of `f`) of `g` is the same as the sum (over the support of `f`) of `h` applied to `g`. In other words, the theorem asserts that the map `h` distributes over the sum operation in `f.sum g`.
Please note that this theorem is deprecated, and you should use `_root_.map_finsupp_sum` instead.
More concisely: For any additive equivalence `h` between commutative monoids `N` and `P`, and any finitely supported function `f` from type `α` to a commutative monoid `M` with zero, the sum of `h` applied to the composition of `g` and `f` is equal to the composition of `h` and the sum of `g` applied to `f`, where `g` is a function from `α` and `M` to `N`.
|
Finsupp.mul_prod_erase
theorem Finsupp.mul_prod_erase :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] (f : α →₀ M) (y : α)
(g : α → M → N), y ∈ f.support → g y (f y) * (Finsupp.erase y f).prod g = f.prod g
The theorem `Finsupp.mul_prod_erase` states that for any finitely supported function `f : α →₀ M`, an element `y` from the support of `f`, and a function `g : α → M → N` (where `N` is a commutative monoid), the product of `g y (f y)` and the product of `g` over `f` with `y` erased is equal to the product of `g` over `f`. In simpler terms, this theorem formalizes the idea of breaking down the product over a set into the product of an element and the product over the set with that element removed.
More concisely: For any commutative monoid N and finitely supported function f : α →₀ M, the product of g(y) * f(y) over y in the support of f, and the product of g over f, are equal.
|
Finsupp.sum_add_index'
theorem Finsupp.sum_add_index' :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] {f g : α →₀ M}
{h : α → M → N},
(∀ (a : α), h a 0 = 0) →
(∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) → (f + g).sum h = f.sum h + g.sum h
The theorem `Finsupp.sum_add_index'` states that given two types `α` and `M`, and an additive commutative monoid `N`, if `h` is a function from `α` and `M` to `N` such that `h` of `a` and `0` is `0` for all `a` in `α`, and `h` of `a` and the sum of `b₁` and `b₂` is the sum of `h` of `a` and `b₁` and `h` of `a` and `b₂` for all `a` in `α` and `b₁`, `b₂` in `M`, then the sum of `h a (f a)` and `h a (g a)` over the support of `f + g` is the sum of `h a (f a)` over the support of `f` and `h a (g a)` over the support of `g`. Here, `f` and `g` are two finitely supported functions from `α` to `M`. This theorem is a more specific version of `finsupp.sum_add_index` with simpler hypotheses, and it shows that taking the sum under `h` is an additive homomorphism of finitely supported functions, if `h` itself is an additive homomorphism.
More concisely: Given two additive commutative monoids `N`, two types `α` and `M`, and a function `h` from `α` x `M` to `N` such that `h(a, 0) = 0` for all `a` in `α` and `h` is additive on `α` x `M`, the sum of `h a (f a)` over the support of `f` is equal to the sum of `h a (g a)` over the support of `g` for any two finitely supported functions `f` and `g` from `α` to `M`.
|
Finsupp.prod_congr
theorem Finsupp.prod_congr :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {f : α →₀ M}
{g1 g2 : α → M → N}, (∀ x ∈ f.support, g1 x (f x) = g2 x (f x)) → f.prod g1 = f.prod g2
The theorem `Finsupp.prod_congr` states that for any types `α`, `M`, `N`, where `M` is a type with a zero and `N` is a commutative monoid, and for any function `f` from `α` to `M` and any two functions `g1` and `g2` from `α` and `M` to `N`, if `g1` and `g2` are equal for all elements in the support of `f`, then the product of `g1` over the support of `f` is equal to the product of `g2` over the support of `f`. Here, the `Finsupp.prod` function is defined as the product of `g a (f a)` over the support of `f`, where `f` is a function from `α` to `M` and `g` is a function from `α` and `M` to `N`.
More concisely: For functions `f: α → M` with `M` being a commutative monoid, and `g1, g2: α × M → N`, if `g1 (x, m) = g2 (x, m)` for all `x ∈ supp (f)` and `m ∈ im (f)`, then `∏ x in supp (f), g1 x (f x) = ∏ x in supp (f), g2 x (f x)`.
|
Finsupp.sum_add_index
theorem Finsupp.sum_add_index :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : DecidableEq α] [inst_1 : AddZeroClass M]
[inst_2 : AddCommMonoid N] {f g : α →₀ M} {h : α → M → N},
(∀ a ∈ f.support ∪ g.support, h a 0 = 0) →
(∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) →
(f + g).sum h = f.sum h + g.sum h
The theorem `Finsupp.sum_add_index` states that for any types `α`, `M`, and `N`, given that `α` has decidable equality, `M` is an additive group with zero, and `N` is an additive commutative monoid, and for any functions `f`, `g` from `α` to `M` and function `h` from `α` and `M` to `N` such that `h` on zero is zero for all elements in the union of the support sets of `f` and `g`, and `h` preserves addition for all elements in the same support set and all elements in `M`, then the sum under `h` over the support set of the sum of `f` and `g` is equal to the sum of the sums under `h` over the support sets of `f` and `g` respectively. In other words, the operation of taking the sum under `h` is an additive homomorphism when restricted to finite support functions, provided `h` is an additive homomorphism on the union of the respective support sets. This is a generalized version of the theorem `Finsupp.sum_add_index'` which has simpler hypotheses.
More concisely: For functions from a decidably equal type to an additive group with zero, and a commutative monoid, if these functions have disjoint support sets and the given function between the monoid and the group preserves addition on common supports and zero at the zero element of the group on support elements, then the sum of the function values on support sets equals the sum of the individual sums.
|
Finsupp.sum_zero
theorem Finsupp.sum_zero :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {f : α →₀ M},
(f.sum fun x x => 0) = 0
The theorem `Finsupp.sum_zero` states that for any type `α`, types `M` and `N` where `M` has an instance of the `Zero` typeclass and `N` has an instance of the `AddCommMonoid` typeclass, and for any function `f` from `α` to `M`, the sum over the support of `f` of the function that constantly returns zero is always zero. In other words, the sum of zeroes over any set (in this case, the support of `f`) is zero.
More concisely: For any function `f` from a type `α` to an additive commutative monoid `M` with a zero element, the sum of `f` evaluated at the zero element of `α` over the support of `f` is equal to the zero element of `M`.
|
Finsupp.onFinset_sum
theorem Finsupp.onFinset_sum :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {s : Finset α}
{f : α → M} {g : α → M → N} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s),
(∀ (a : α), g a 0 = 0) → (Finsupp.onFinset s f hf).sum g = s.sum fun a => g a (f a)
The theorem `Finsupp.onFinset_sum` states that for any types `α`, `M`, and `N`, given a zero element in `M`, an associative and commutative addition operation in `N`, a finite set `s` of elements of type `α`, a function `f` mapping elements of `α` to `M`, and a function `g` mapping pairs of `α` and `M` to `N`, if `f` is nonzero only on elements in `s`, and `g` maps any `α` paired with `0` to `0`, then the sum of `g`, when applied to the function represented by `f` restricted to `s` using `Finsupp.onFinset`, is equal to the sum of `g`, when applied directly to `f` and the elements in the original finite set `s`. This effectively asserts that using `Finsupp.onFinset` to restrict the function to a set does not change the result of summing over the function using `g`.
More concisely: Given a zero element in `M`, an associative and commutative addition operation in `N`, a finite set `s` of elements of type `α`, a function `f : α → M`, and a function `g : α × M → N`, if `f` is zero outside of `s` and `g(_, 0) = 0`, then `∑ (x : α) in s, g(x, f x) = ∑ (x : α) in s, g(x, (Finsupp.onFinset s f) x)`.
|
Finsupp.prod_add_index
theorem Finsupp.prod_add_index :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : DecidableEq α] [inst_1 : AddZeroClass M]
[inst_2 : CommMonoid N] {f g : α →₀ M} {h : α → M → N},
(∀ a ∈ f.support ∪ g.support, h a 0 = 1) →
(∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) →
(f + g).prod h = f.prod h * g.prod h
The theorem `Finsupp.prod_add_index` states that for any types `α`, `M`, and `N`, given `α` has decidable equality, `M` is an additive zero class, and `N` is a commutative monoid, for any functions `f` and `g` from `α` to `M` and any function `h` from `α` and `M` to `N`, if `h` maps any element `a` in the union of the supports of `f` and `g` and `0` to `1`, and for any elements `b₁` and `b₂` in `M`, `h` maps `a` and the sum of `b₁` and `b₂` to the product of `h` mapping `a` and `b₁` and `h` mapping `a` and `b₂`, then the product of `f + g` under `h` equals the product of the product of `f` under `h` and the product of `g` under `h`. In other words, under these conditions, taking the product under `h` transforms the addition of `f` and `g` into the multiplication of their products, demonstrating the homomorphism from additive to multiplicative of finite support functions. This is a more general version of the theorem `Finsupp.prod_add_index'`, which has simpler hypotheses.
More concisely: Given types `α`, `M`, and `N` with decidable equality on `α`, `M` an additive zero class, and `N` a commutative monoid, for functions `f` and `g` from `α` to `M` and `h` from `α × M` to `N` such that `h(a, 0) = 1` for all `a` in the union of the supports of `f` and `g`, if `h` satisfies `h(a, b₁ + b₂) = h(a, b₁) * h(a, b₂)` for all `a` and `b₁, b₂` in `M`, then `(∫ x in ℕ, h (x, (f + g)(x))) = (∫ x in ℕ, h (x, f(x))) * (∫ x in ℕ, h (x, g(x)))`.
|
Finsupp.support_sum
theorem Finsupp.support_sum :
∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : DecidableEq β] [inst_1 : Zero M]
[inst_2 : AddCommMonoid N] {f : α →₀ M} {g : α → M → β →₀ N},
(f.sum g).support ⊆ f.support.biUnion fun a => (g a (f a)).support
The theorem `Finsupp.support_sum` states that for any types `α`, `β`, `M`, and `N`, given decidable equality on `β`, a zero element in `M`, and an additive commutative monoid structure on `N`, and for any function `f` from `α` to `M` and a function `g` from `α` and `M` to `β` with finite support, the support of the sum `Finsupp.sum f g` is a subset of the union of the supports of `g a (f a)` for each `a` in the support of `f`. This means that all elements contributing to the sum `Finsupp.sum f g` come from these supports.
More concisely: For any decidably equal types `α`, `β`, additive commutative monoids `M` and `N`, given a zero element `0_M` in `M`, a function `g : α × M → β` with finite support, and a function `f : α → M`, the support of the sum `Finsupp.sum f g` is contained in the union of the supports of `g (a, f(a))` for all `a` in the support of `f`.
|
MulEquiv.map_finsupp_prod
theorem MulEquiv.map_finsupp_prod :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [inst : Zero M] [inst_1 : CommMonoid N]
[inst_2 : CommMonoid P] (h : N ≃* P) (f : α →₀ M) (g : α → M → N), h (f.prod g) = f.prod fun a b => h (g a b)
The theorem `MulEquiv.map_finsupp_prod` states that for any types `α`, `M`, `N`, and `P`, given an instance of zero for `M`, and commutative monoid instances for `N` and `P`, for any multiplicative equivalence `h` from `N` to `P`, and any finite support function `f` that maps from `α` to `M`, and any function `g` that maps from `α` and `M` to `N`, the result of applying `h` to the product of `f` and `g` is equivalent to the product of `f` and the function that takes `a` and `b` and applies `h` to `g(a, b)`. Note that the theorem is deprecated and `_root_.map_finsupp_prod` should be used instead.
More concisely: Given commutative monoids N and P, multiplicative equivalence h from N to P, a finite support function f from α to M, and a function g from α × M to N, the product of f and g is equivalent to the function that applies h to the product of g with the projection function from M to 1 in N.
|
Nat.prod_pow_pos_of_zero_not_mem_support
theorem Nat.prod_pow_pos_of_zero_not_mem_support : ∀ {f : ℕ →₀ ℕ}, 0 ∉ f.support → 0 < f.prod fun x x_1 => x ^ x_1 := by
sorry
The theorem `Nat.prod_pow_pos_of_zero_not_mem_support` states that for any function `f` mapping from natural numbers to natural numbers, if the value `0` is not in the support of `f` (meaning `f` does not map any element to `0`), then the product of each element in the support of `f`, raised to the power of its corresponding image under `f`, is strictly greater than zero. This product is taken over all elements `x` in the support of `f` with each term being `x` to the power of `f(x)`.
More concisely: If a function `f` from natural numbers to natural numbers maps no element to `0`, then the product of each element in the support of `f` raised to the power of its image under `f` is strictly positive.
|
MonoidHom.map_finsupp_prod
theorem MonoidHom.map_finsupp_prod :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [inst : Zero M] [inst_1 : CommMonoid N]
[inst_2 : CommMonoid P] (h : N →* P) (f : α →₀ M) (g : α → M → N), h (f.prod g) = f.prod fun a b => h (g a b)
This theorem, which is now deprecated and recommends to use `_root_.map_finsupp_prod` instead, states that for any types `α`, `M`, `N`, and `P`, given a monoid homomorphism `h` from `N` to `P`, a function `g` from tuples of `α` and `M` to `N`, and a finite support function `f` from `α` to `M`, the application of `h` to the product of `f` and `g` is the same as the product of `f` and the function that applies `h` to `g` for each tuple of `α` and `M`. Here, `M` is a type with a zero element, and `N` and `P` are both commutative monoids.
More concisely: For any commutative monoids N and P, monoid homomorphism h from N to P, function g from tuples of alpha and M to N, and finite support function f from alpha to M, we have h (f ⊤ g) = (f ⊤ (h ∘ g)).
|
Finsupp.sum_eq_single
theorem Finsupp.sum_eq_single :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {f : α →₀ M} (a : α)
{g : α → M → N}, (∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 0) → (f a = 0 → g a 0 = 0) → f.sum g = g a (f a)
The theorem `Finsupp.sum_eq_single` states that for any types `α`, `M`, and `N` where `M` has a zero element and `N` is an additive commutative monoid, and for any function `f` from `α` to `M`, any element `a` of type `α`, and any function `g` from `α` and `M` to `N`, if `g` applied to `b` and `f b` is zero for all `b` not equal to `a` where `f b` is not zero, and if `g a 0` is zero when `f a` is zero, then the sum of `g a (f a)` over the support of `f`, as defined by `Finsupp.sum f g`, is equal to `g a (f a)`. In other words, the sum of the function `g` applied to each element `a` and its corresponding `f a` over the support of `f` is essentially determined by the value of `g a (f a)`.
More concisely: For any function `f: α -> M` from a type `α` to an additive commutative monoid `M` with zero element, and any function `g: α x M -> N` from `α` and `M` to another additive commutative monoid `N`, if the sum of `g a (f a)` over the support of `f` equals `g a (f a)` for all `a` where `f a` is non-zero, then the sum of `g` applied to each `(a, f a)` pair over the support of `f` equals `g a (f a)`.
|
Finsupp.prod_mapRange_index
theorem Finsupp.prod_mapRange_index :
∀ {α : Type u_1} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [inst : Zero M] [inst_1 : Zero M']
[inst_2 : CommMonoid N] {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h : α → M' → N},
(∀ (a : α), h a 0 = 1) → (Finsupp.mapRange f hf g).prod h = g.prod fun a b => h a (f b)
This theorem, `Finsupp.prod_mapRange_index`, states that for any types `α`, `M`, `M'`, `N`, a function `f` from `M` to `M'` such that `f` of `0` equals `0`, a finitely supported function `g` from `α` to `M`, a function `h` from `α` to `N`, if `h` of any `α` and `0` equals `1`, then the product over the support of `g` mapped through `f` with function `h` is equal to the product over the support of `g` with `h` composed with `f`.
In mathematical terms, for all `a` in the support of `g`, we have the equality $\prod_{a \in \text{supp}(g)} h(a, f(g(a))) = \prod_{a \in \text{supp}(g)}h(a, g(a))$ when we consider `f` applied to the output of `g`. Here, `Finsupp.prod` represents the product of `h a (f a)` over the support of `g` and `Finsupp.mapRange` maps the range of `g` through `f`.
More concisely: For any finitely supported functions `g: α → M` and `h: α → N`, if `h 0 = 1` and `f: M → M'` maps `0` to `0`, then the product of `h` composed with `g` over `g`'s support is equal to the product of `h` over the support of `g` and `f` applied to the product of `h` and `g`.
|
Finsupp.sum_of_support_subset
theorem Finsupp.sum_of_support_subset :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] (f : α →₀ M)
{s : Finset α}, f.support ⊆ s → ∀ (g : α → M → N), (∀ i ∈ s, g i 0 = 0) → f.sum g = s.sum fun x => g x (f x)
The theorem `Finsupp.sum_of_support_subset` states that for every type `α`, `M`, and `N`, given a zero of type `M`, an additive commutative monoid of type `N`, a function `f` from `α` to `M` and a finite set `s` of `α`, if the support of `f` (i.e., the set of elements where `f` is non-zero) is a subset of `s`, then for any function `g` from `α` to the function space from `M` to `N`, such that `g` of `i` and `0` equals `0` for all `i` in `s`, the sum of `g a (f a)` over the support of `f` equals the sum of `g x (f x)` as `x` ranges over the elements of the finite set `s`.
More concisely: If `f` is a function from a set `α` to a commutative additive monoid `M`, with finite support `s`, and `g` is a function from `α` to the function space from `M` to a commutative additive monoid `N`, such that `g i (0) = 0` for all `i` in `s`, then the sum of `g i (f i)` over `i` in `s` equals the sum of `g x (f x)` over `x` in `s`.
|
Finsupp.liftAddHom_apply_single
theorem Finsupp.liftAddHom_apply_single :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (f : α → M →+ N)
(a : α) (b : M), ((Finsupp.liftAddHom f) fun₀ | a => b) = (f a) b
This theorem states that for any types `α`, `M`, and `N`, given an additive commutative monoid structure on `M` and `N`, and a function `f` from `α` to the additive monoid homomorphisms from `M` to `N`, for any `a` of type `α` and any `b` of type `M`, applying `Finsupp.liftAddHom` on `f` and then applying this to a function `fun₀` (which is a function from `α` to `M` that is zero for all inputs except for `a` where it returns `b`) is equal to applying `f` at `a` and then applying this to `b`. The `Finsupp.liftAddHom` function is a way of lifting a function to operate on finitely supported functions, which are functions that are zero except at finitely many points.
More concisely: For any additive commutative monoids M and N, and any function f from type α to additive monoid homomorphisms from M to N, the application of Finsupp.liftAddHom(f) to the function fun₀ from α to M, which is zero everywhere except for mapping a to b, is equal to the composition of applying f to a and then applying it to b.
|
Finsupp.onFinset_prod
theorem Finsupp.onFinset_prod :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {s : Finset α} {f : α → M}
{g : α → M → N} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s),
(∀ (a : α), g a 0 = 1) → (Finsupp.onFinset s f hf).prod g = s.prod fun a => g a (f a)
The theorem `Finsupp.onFinset_prod` states that for all types `α`, `M`, and `N`, given a zero instance for `M` and a commutative monoid instance for `N`, for any finite set `s` of type `α`, any function `f` from `α` to `M`, and any function `g` from `α` and `M` to `N`, if `f` is non-zero only for members of `s` and `g` maps a second argument of 0 to 1, then the product of `g` applied to the result of `f` restricted to `s` (using `Finsupp.onFinset`) is equal to the product of `g` applied to `f` over the original set `s`. In mathematical terms, this is $\prod_{a \in s} g(a, f(a)) = \prod_{a \in s} g(a, (Finsupp.onFinset \, s \, f \, hf)(a))$.
More concisely: For any finite set $s$, function $f : \alpha \to M$, and commutative monoid $N$ with zero element $0_N$, if $f$ is non-zero only on $s$ and $g : \alpha \times M \to N$ maps the second argument to $1$ for $0_M$, then $\prod_{a \in s} g(a, f(a)) = \prod_{a \in s} g(a, (Finsupp.onFinset \, s \, f \, hf)(a))$.
|
Finsupp.univ_sum_single
theorem Finsupp.univ_sum_single :
∀ {α : Type u_1} {M : Type u_8} [inst : Fintype α] [inst_1 : AddCommMonoid M] (f : α →₀ M),
(Finset.univ.sum fun a => fun₀ | a => f a) = f
This theorem, `Finsupp.univ_sum_single`, states that for any given type `α` (with finiteness property) and another type `M` (with addition and commutativity properties), for a function `f` from `α` to `M` that belongs to `Finsupp` (a type of functions with finite support), the sum of the function values over all elements in the universal set `Finset.univ` (which includes all elements of the finitely sized type `α`) is equal to the function `f` itself. In essence, this is a property related to the sum of a function over a universal set in the context of finite support functions.
More concisely: For any type `α` with finiteness property, type `M` with additive commutativity, and `f : α → M` in `Finsupp`, the sum of `f` over `Finset.univ` equals `f`.
|
Finsupp.prod_ite_eq'
theorem Finsupp.prod_ite_eq' :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] [inst_2 : DecidableEq α]
(f : α →₀ M) (a : α) (b : α → M → N),
(f.prod fun x v => if x = a then b x v else 1) = if a ∈ f.support then b a (f a) else 1
This theorem, known as `Finsupp.prod_ite_eq'`, is a variant of `prod_ite_eq` but with the equality test reversed. It states that for any types `α`, `M`, and `N` with `M` being a type with a zero element, `N` a type with commutative monoid structure, and `α` having decidable equality. For any function `f` from `α` to `M`, any element `a` of `α`, and any function `b` from `α` and `M` to `N`, the product of `f`, where each term is `b(x, f(x))` if `x = a` and is `1` otherwise, equals `b(a, f(a))` if `a` is in the support of `f` and `1` otherwise. The support of a function is the set of points where the function is non-zero.
More concisely: For functions from type `α` to type `M` with `M` having a zero element and commutative monoid structure and `α` having decidable equality, the product of such a function `f` with a function `b` from `α × M` to `N` equals `b(a, f(a))` if `a` is in the support of `f`, and `1` otherwise.
|
Finsupp.sum_add_index_of_disjoint
theorem Finsupp.sum_add_index_of_disjoint :
∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] {f1 f2 : α →₀ M},
Disjoint f1.support f2.support →
∀ {β : Type u_16} [inst_1 : AddCommMonoid β] (g : α → M → β), (f1 + f2).sum g = f1.sum g + f2.sum g
The theorem `Finsupp.sum_add_index_of_disjoint` states that for any two functions `f1` and `f2` whose supports are disjoint, and any given function `g`, the sum of the function `g` evaluated over `f1 + f2` equals the sum of `g` evaluated over `f1` plus the sum of `g` evaluated over `f2`. Here, the term "support" of a function refers to the set of points where the function is non-zero, and the term "disjoint" means that the supports of `f1` and `f2` do not intersect. The functions `f1` and `f2` map from type `α` to an additive commutative monoid `M`, and the function `g` is a binary function from `α` and `M` to another additive commutative monoid `β`.
More concisely: For functions `f1` and `f2` with disjoint supports mapping from type `α` to an additive commutative monoid `M`, and a binary function `g` from `α × M` to another additive commutative monoid `β`, we have `∑ (x : α) (g x (f1 x + f2 x)) = ∑ (x : α) g x (f1 x) + ∑ (x : α) g x (f2 x)`.
|
Finsupp.sum_ite_eq'
theorem Finsupp.sum_ite_eq' :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] [inst_2 : DecidableEq α]
(f : α →₀ M) (a : α) (b : α → M → N),
(f.sum fun x v => if x = a then b x v else 0) = if a ∈ f.support then b a (f a) else 0
The theorem `Finsupp.sum_ite_eq'` states that for any types `α`, `M`, and `N`, given an instance of `Zero M`, `AddCommMonoid N` and decidable equality on `α`, for any function `f` from `α` to `M`, any element `a` of `α`, and any function `b` from `α` and `M` to `N`, the sum of the function defined by `(if x = a then b x v else 0)` evaluated at all points `(x, v)` in the domain of `f` is equal to `b a (f a)` if `a` is in the support of `f` (i.e., `f a ≠ 0`), and 0 otherwise. In other words, it sums up the values of the function `b` applied to `a` and `f a` over all elements `a` in the support of `f`, and gives 0 for all other elements.
More concisely: For any types `α`, `M`, and `N` with Zero `M`, AddCommMonoid `N`, and decidable equality on `α`, the sum of the function `(x mapsto if x = a then b x else 0)` over the domain of a function `f` from `α` to `M` equals `b a (f a)` if `a` is in the support of `f`, and 0 otherwise.
|
RingHom.map_finsupp_prod
theorem RingHom.map_finsupp_prod :
∀ {α : Type u_1} {M : Type u_8} {R : Type u_14} {S : Type u_15} [inst : Zero M] [inst_1 : CommSemiring R]
[inst_2 : CommSemiring S] (h : R →+* S) (f : α →₀ M) (g : α → M → R),
h (f.prod g) = f.prod fun a b => h (g a b)
This theorem states that for any given types `α`, `M`, `R`, and `S`, where `M` is a type with a zero element, and `R` and `S` are commutative semirings, a ring homomorphism `h` from `R` to `S`, a function `f` that maps type `α` to a finitely supported function from `α` to `M`, and a function `g` that maps `α` and `M` to `R`, the result of applying `h` to the product of `f` and `g` (using the `prod` function on finitely supported functions) is equal to the product of `f` and the function that maps an element of `α` and an element of `M` to the result of applying `h` to `g` applied to the same elements. Please note that this theorem is deprecated and the `_root_.map_finsupp_prod` should be used instead.
More concisely: Given types `α`, `M` with a zero element, commutative semirings `R` and `S`, a ring homomorphism `h` from `R` to `S`, a function `f: α → ∇(M)` mapping `α` to finitely supported functions from `M` to `M`, and a function `g: α × M → R`, the map-distributive property holds: `h (∏(x ∈ α) f x ⊤ (g x, m)) = ∏(x ∈ α) (λ (x : α), h (g x, m)) (f x)`, where `∏` denotes the product of functions and `⊤` is the constant function with value `one_R` (the multiplicative identity of `R`).
|
Finsupp.prod_of_support_subset
theorem Finsupp.prod_of_support_subset :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] (f : α →₀ M) {s : Finset α},
f.support ⊆ s → ∀ (g : α → M → N), (∀ i ∈ s, g i 0 = 1) → f.prod g = s.prod fun x => g x (f x)
This theorem states that for any function `f` from a type `α` to a type `M` where `M` has a zero element, and for any finite set `s` of elements of type `α`, if the support of `f` (the set of elements where `f` is non-zero) is a subset of `s`, then for any function `g` from `α` and `M` to a type `N` (where `N` forms a commutative monoid), and provided `g` maps any element of `s` and the zero element to the identity element of the commutative monoid `N`, the product of `g a (f a)` over the support of `f` is equal to the product of `g x (f x)` where `x` ranges over the elements of the finite set `s`.
More concisely: For any function `f` from type `α` to a commutative monoid `M` with a zero element, and any finite set `s` of `α` containing the support of `f`, if `g` is a function from `α x M` to a commutative monoid `N` mapping `s` and the zero element to the identity, then the product of `g (a, f a)` over the support of `f` equals the product of `g (x, f x)` for all `x` in `s`.
|
AddMonoidHom.map_finsupp_sum
theorem AddMonoidHom.map_finsupp_sum :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [inst : Zero M] [inst_1 : AddCommMonoid N]
[inst_2 : AddCommMonoid P] (h : N →+ P) (f : α →₀ M) (g : α → M → N), h (f.sum g) = f.sum fun a b => h (g a b)
The theorem `AddMonoidHom.map_finsupp_sum` states that for any types `α`, `M`, `N`, and `P`, given a zero element for type `M`, additive commutative monoid structures for types `N` and `P`, a map `h` from `N` to `P` that preserves addition, a function `f` from `α` to `M` represented as a finite sum with coefficients, and a function `g` from `α × M` to `N`, applying `h` to the sum of `f` evaluated with `g` is the same as the sum of applying `h` to `g` applied to `a` and `b` over the support of `f`. Simply put, this theorem is a mapping property of finite sums in the context of additive monoid homomorphisms. Note that this theorem is deprecated and `_root_.map_finsupp_sum` should be used instead.
More concisely: For any additive commutative monoids N and P, additive monoid homomorphism h from N to P, function f from α to M represented as a finite sum with coefficients, and function g from α × M to N, h(∑(a ∈ α) f(a) + g(a, _)) = ∑(a ∈ α) h(g(a, f(a))).
|
map_finsupp_sum
theorem map_finsupp_sum :
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [inst : Zero M] [inst_1 : AddCommMonoid N]
[inst_2 : AddCommMonoid P] {H : Type u_16} [inst_3 : FunLike H N P] [inst_4 : AddMonoidHomClass H N P] (h : H)
(f : α →₀ M) (g : α → M → N), h (f.sum g) = f.sum fun a b => h (g a b)
The theorem `map_finsupp_sum` states that for any types `α`, `M`, `N`, `P`, and `H`, given the conditions that `M` has a zero element, `N` and `P` have a commutative addition operation, `H` is a function-like object from `N` to `P`, and `H` is also a kind of additive monoid homomorphism between `N` and `P`, then for any `h` of type `H`, any function `f` from `α` to `M` with finite support, and any function `g` from `α` and `M` to `N`, applying `h` to the sum of `g a (f a)` over the support of `f` is equal to the sum of `h (g a b)` over the support of `f`. This is essentially a statement about being able to interchange the order of summation and the application of the function `h`.
More concisely: For any commutative additive monoids (N, +) and (P, +), function-like object H from N to P that is an additive monoid homomorphism, and functions f from α to M with finite support and g from α and M to N, the following equality holds: h (∑i ∈ supp(f) g i (f i)) = ∑i ∈ supp(f) h (g i (f i)).
|
Finsupp.prod_add_index_of_disjoint
theorem Finsupp.prod_add_index_of_disjoint :
∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] {f1 f2 : α →₀ M},
Disjoint f1.support f2.support →
∀ {β : Type u_16} [inst_1 : CommMonoid β] (g : α → M → β), (f1 + f2).prod g = f1.prod g * f2.prod g
The theorem `Finsupp.prod_add_index_of_disjoint` states that for any given types `α` and `M` where `M` is an additive commutative monoid, given two functions `f1` and `f2` from `α` to `M`, if the support sets of `f1` and `f2` are disjoint (i.e., their greatest lower bound is the bottom element of the lattice), then for any type `β` that is a commutative monoid, and any function `g` from `α` and `M` to `β`, the product of `g` over the sum of `f1` and `f2` is equal to the product of the products of `g` over `f1` and `f2` individually. In other words, it's asserting a kind of distributive property for the product operation over the sum of disjoint functions.
More concisely: For functions `f1` and `f2` from a type `α` to an additive commutative monoid `M` with disjoint support sets, and a function `g` from `α` x `M` to a commutative monoid `β`, the product of `g` over the sum of `f1` and `f2` equals the product of the separate products of `g` over `f1` and `f2`.
|