Big operators for finsupps #
This file contains theorems relevant to big operators in finitely supported functions.
Declarations about Finsupp.sum
and Finsupp.prod
#
In most of this section, the domain β
is assumed to be an AddMonoid
.
The left hand side of sum_ite_self_eq
simplifies; this is the variant that is useful for simp
.
A restatement of prod_ite_eq
with the equality test reversed.
A restatement of sum_ite_eq
with the equality test reversed.
A restatement of sum_ite_self_eq
with the equality test reversed.
If g
maps a second argument of 0 to 1, then multiplying it over the
result of onFinset
is the same as multiplying it over the original Finset
.
If g
maps a second argument of 0 to 0, summing it over the
result of onFinset
is the same as summing it over the original Finset
.
Taking a product over f : α →₀ M
is the same as multiplying the value on a single element
y ∈ f.support
by the product over erase y f
.
Taking a sum over f : α →₀ M
is the same as adding the value on a
single element y ∈ f.support
to the sum over erase y f
.
Generalization of Finsupp.mul_prod_erase
: if g
maps a second argument of 0 to 1,
then its product over f : α →₀ M
is the same as multiplying the value on any element
y : α
by the product over erase y f
.
Generalization of Finsupp.add_sum_erase
: if g
maps a second argument of 0
to 0, then its sum over f : α →₀ M
is the same as adding the value on any element
y : α
to the sum over erase y f
.
Taking the product under h
is an additive-to-multiplicative homomorphism of finsupps,
if h
is an additive-to-multiplicative homomorphism on the support.
This is a more general version of Finsupp.prod_add_index'
; the latter has simpler hypotheses.
Taking the product under h
is an additive homomorphism of finsupps, if h
is an
additive homomorphism on the support. This is a more general version of
Finsupp.sum_add_index'
; the latter has simpler hypotheses.
Taking the product under h
is an additive-to-multiplicative homomorphism of finsupps,
if h
is an additive-to-multiplicative homomorphism.
This is a more specialized version of Finsupp.prod_add_index
with simpler hypotheses.
Taking the sum under h
is an additive homomorphism of finsupps,if h
is an additive
homomorphism. This is a more specific version of Finsupp.sum_add_index
with simpler
hypotheses.
The canonical isomorphism between families of additive monoid homomorphisms α → (M →+ N)
and monoid homomorphisms (α →₀ M) →+ N
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Finsupp
version of Finset.univ_sum_single
For disjoint f1
and f2
, and function g
, the product of the products of g
over f1
and f2
equals the product of g
over f1 + f2
For disjoint f1
and f2
, and function g
, the sum of the sums of g
over f1
and f2
equals the sum of g
over f1 + f2
Version of Finsupp.apply'
that applies in large generality to linear combinations
of functions in any FunLike
type on which addition is defined pointwise.
At the time of writing Mathlib does not have a typeclass to express the condition
that addition on a FunLike
type is pointwise; hence this is asserted via explicit hypotheses.