Finset.sum_smul
theorem Finset.sum_smul :
∀ {ι : Type u_1} {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{f : ι → R} {s : Finset ι} {x : M}, (s.sum fun i => f i) • x = s.sum fun i => f i • x
The theorem `Finset.sum_smul` states that for any type `R` equipped with a semiring structure, any type `M` equipped with an additively commutative monoid structure and a module structure over `R`, a function `f` from a type `ι` to `R`, a finite set `s` of type `ι`, and an element `x` of type `M`, the scalar multiplication of the sum of the function `f` applied to all elements in `s` by `x` is equal to the sum over `s` of the scalar multiplication of `x` by `f i` for each element `i` in `s`. In mathematical terms, it states that $\left(\sum_{i \in s} f(i)\right) \cdot x = \sum_{i \in s} (f(i) \cdot x)$, where the sum is over a finite set `s`.
More concisely: For any semiring `R`, additively commutative monoid `M` with an `R`-module structure, function `f` from a type `ι` to `R`, finite set `s` of type `ι`, and element `x` of type `M`, we have $\sum\_{i \in s} (f(i) \cdot x) = (\sum\_{i \in s} f(i)) \cdot x$.
|
Finset.cast_card
theorem Finset.cast_card :
∀ {α : Type u_3} {R : Type u_5} [inst : CommSemiring R] (s : Finset α), ↑s.card = s.sum fun a => 1
The theorem `Finset.cast_card` states that for any type `α` and a type `R` where `R` is a commutative semiring, for any given finite set `s` of type `α`, the cardinality of `s` (the number of elements in set `s`) is equal to the sum of `1` for each element in `s`. In other words, if you sum up `1` for each element in the finite set `s`, you get the total number of elements in `s`.
More concisely: For any finite set `s` of type `α` and commutative semiring `R`, the cardinality of `s` equals the sum of `1` for each element in `s` (denoted as the sum of the elements in the set viewed as an `R`-module).
|