Finset.univ_sum_single
theorem Finset.univ_sum_single :
∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_2} [inst_1 : (i : I) → AddCommMonoid (Z i)]
[inst_2 : Fintype I] (f : (i : I) → Z i), (Finset.univ.sum fun i => Pi.single i (f i)) = f
The theorem `Finset.univ_sum_single` states that for any type `I` with decidable equality, a function `Z` mapping from `I` to another type, an additive commutative monoid structure on `Z i` for each `i` in `I`, a `Fintype` instance for `I`, and a function `f` mapping from `I` to `Z i`, the sum, over all elements in the universal finite set of `I`, of the function 'single' applied to `i` and `f(i)`, is equal to `f`. The function 'single' here is defined as the function which takes a value `x` at `i` and `0` elsewhere. In mathematical terms, this theorem is stating that the sum of a function over all elements in a finite set is equal to the function itself when the function is equal to a given constant at only one point in the set and zero elsewhere.
More concisely: For any finite type `I` with decidable equality, a function `Z : I -> AddMonoid a`, a Fintype instance for `I`, and a function `f : I -> Z i`, the sum of the constant function `single i 0` over `I` is equal to `f` if `f` is constant on `I` with value `0` everywhere except for `i`.
|
Finset.sum_fn
theorem Finset.sum_fn :
∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : (a : α) → AddCommMonoid (β a)] (s : Finset γ)
(g : γ → (a : α) → β a), (s.sum fun c => g c) = fun a => s.sum fun c => g c a
This theorem, `Finset.sum_fn`, is an unapplied analogue of `Finset.sum_apply`. For any types `α`, `β` (which is a function of `α`), and `γ`, if we have an additive commutative monoid structure on `β a` for any `a : α`, a finite set `s` of type `γ`, and a function `g` that maps an element of `γ` to a function from `α` to `β a`, then the sum over `s` of the function `g c` (for `c` in `s`) is equal to a function that, for each `a : α`, gives the sum over `s` of `g c a`. In other words, it expresses a re-arrangement of the order of summation in a double sum.
More concisely: For any additive commutative monoid `β` over types `α`, given a finite set `s` of type `γ`, a function `g : γ → α → β`, and assuming `β a` is an additive commutative monoid for each `a : α`, the function sum over `s` of `g c` is equal to the function that maps each `a : α` to the sum over `s` of `g c a`.
|
Finset.prod_fn
theorem Finset.prod_fn :
∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : (a : α) → CommMonoid (β a)] (s : Finset γ)
(g : γ → (a : α) → β a), (s.prod fun c => g c) = fun a => s.prod fun c => g c a
This theorem, `Finset.prod_fn`, is about the product operation on finite sets in Lean. For any types `α`, `β` and `γ`, and a commutative monoid structure on `β a` for every `α a`, if `s` is a finite set of type `γ` and `g` is a function from `γ` to functions from `α` to `β a`, then the product over `s` of `g c` (for `c` in `s`) is equal to a function from `α` to the product over `s` of `g c a` (for `c` in `s`). Essentially, this theorem allows us to interchange the order of two operations: taking a product over a finite set and applying a function.
More concisely: For any commutative monoids `β` indexed over types `α`, given a finite set `s` of type `γ` and a function `g : γ → (α → β)`, the function `∏ (α × s) (λ (a, c), g c a)` is equal to `λ x, ∏ (s, α) (λ (c, a), g c a) x`.
|
AddMonoidHom.functions_ext'
theorem AddMonoidHom.functions_ext' :
∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_2} [inst_1 : (i : I) → AddCommMonoid (Z i)]
[inst_2 : Finite I] (M : Type u_3) [inst_3 : AddCommMonoid M] (g h : ((i : I) → Z i) →+ M),
(∀ (i : I), g.comp (AddMonoidHom.single Z i) = h.comp (AddMonoidHom.single Z i)) → g = h
This theorem, `AddMonoidHom.functions_ext'`, states that for any type `I` with decidable equality, any dependent type `Z` indexed by `I` where each `Z i` is an additive commutative monoid, when `I` is finite, and any type `M` that is also an additive commutative monoid, for any two additive monoid homomorphisms `g` and `h` from functions `I → Z i` to `M`, if for all `i` in `I`, the composition of `g` (or `h`) with the additive monoid homomorphism from `Z i` to functions `I → Z i` that is supported at `i` is equal, then `g` and `h` themselves are equal. In simpler terms, two additive monoid homomorphisms are equal if their compositions with the function embedding each `Z i` into the dependent family `I → Z i` are equal for all `i` in `I`.
More concisely: For any finite index type `I` with decidable equality, if two functions `g` and `h` from `I` to an additive commutative monoid `M` are additive monoid homomorphisms such that the composition of each with the embedding of each `Z i` into `I → Z i` is equal, then `g` and `h` are equal.
|
MonoidHom.functions_ext'
theorem MonoidHom.functions_ext' :
∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_2} [inst_1 : (i : I) → CommMonoid (Z i)] [inst_2 : Finite I]
(M : Type u_3) [inst_3 : CommMonoid M] (g h : ((i : I) → Z i) →* M),
(∀ (i : I), g.comp (MonoidHom.mulSingle Z i) = h.comp (MonoidHom.mulSingle Z i)) → g = h
This theorem, `MonoidHom.functions_ext'`, states that for any type `I` with a decidable equality, any type-dependent `Z` with each `Z i` being a commutative monoid, any finite `I`, any type `M` also being a commutative monoid, and any two monoid homomorphisms `g` and `h` from the function type `(i : I) → Z i` to `M`, if for every `i` in `I`, the composition of `g` and `MonoidHom.mulSingle Z i` is equal to the composition of `h` and `MonoidHom.mulSingle Z i`, then `g` and `h` must be equal.
In simpler terms, it tells us that if two monoid homomorphisms behave identically when composed with the function `MonoidHom.mulSingle Z i` for every `i`, then they must be the same homomorphisms. This theorem is primarily used for extensionality arguments in proofs involving monoid homomorphisms.
More concisely: If two monoid homomorphisms from a type-dependent commutative monoid to another commutative monoid agree on the compositions with the monoid multiplication functions for all elements, then they are equal.
|
AddMonoidHom.functions_ext
theorem AddMonoidHom.functions_ext :
∀ {I : Type u_1} [inst : DecidableEq I] {Z : I → Type u_2} [inst_1 : (i : I) → AddCommMonoid (Z i)]
[inst_2 : Finite I] (G : Type u_3) [inst_3 : AddCommMonoid G] (g h : ((i : I) → Z i) →+ G),
(∀ (i : I) (x : Z i), g (Pi.single i x) = h (Pi.single i x)) → g = h
This theorem, `AddMonoidHom.functions_ext`, asserts that for a finite index set `I` with decidable equality and a type `Z` indexed by `I` such that each `Z i` forms an additive commutative monoid, given another type `G` that also forms an additive commutative monoid, if we have two additive monoid homomorphisms `g` and `h` from the function space `(i : I) → Z i` to `G`, then these two homomorphisms are equal if and only if they map each individual function `Pi.single i x` (a function supported at `i` with value `x` there, and `0` elsewhere) to the same value in `G` for all `i` in `I` and `x` in `Z i`.
More concisely: Given a finite indexed set I with decidable equality, types Z indexed by I forming additive commutative monoids, and type G also forming an additive commutative monoid, two additive monoid homomorphisms from the function space (i : I) -> Z i to G are equal if and only if they map each Pi.single i x to the same value in G for all i in I and x in Z i.
|
Finset.prod_apply
theorem Finset.prod_apply :
∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : (a : α) → CommMonoid (β a)] (a : α) (s : Finset γ)
(g : γ → (a : α) → β a), s.prod (fun c => g c) a = s.prod fun c => g c a
The theorem `Finset.prod_apply` states that for all types `α`, `β` which is a function of `α`, and `γ`, along with a commutative monoid structure on `β a` for every `a` in `α`, a specific `a` in `α`, a finite set `s` of `γ`, and a function `g` mapping from `γ` to `β a`, the product of the function `g` over the set `s` applied to `a` is equal to the product over the set `s` of the function `g c a`.
In other words, when computing the product of the function `g` over all elements in the finite set `s` and then applying this to `a`, it's the same as computing the product over the set `s` of the function `g` applied to each element `c` and `a`.
More concisely: For any commutative monoid `β` over type `α`, function `g` from `γ` to `β a`, and finite set `s` of `γ`, the product of `g` over `s` and applied to `a` equals the product over `s` of `g a` applied to each element in `s`.
|
Finset.sum_apply
theorem Finset.sum_apply :
∀ {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [inst : (a : α) → AddCommMonoid (β a)] (a : α) (s : Finset γ)
(g : γ → (a : α) → β a), s.sum (fun c => g c) a = s.sum fun c => g c a
The theorem `Finset.sum_apply` states that for all types `α`, `β` (which is a function from `α`), and `γ`, and for a particular `α` instance `a` and a finite set `s` of type `γ`, if the additive commutative monoid structure is given for each `β a`, then the sum over the set `s` of applying the function `g` (which takes an element of `γ` and returns a function from `α` to `β a`), and then applying `a`, equals to the sum over the set `s` of applying `g` to an element of `s` and then applying `a`. In other words, it verifies the interchangeability of summing and function application.
More concisely: For any types `α`, `β`, and `γ`, given a finite set `s` of type `γ`, an additive commutative monoid structure on `β`, and a function `g : γ -> (α -> β a)`, the sum of applying `g` to each element in `s` and then applying `a` is equal to the sum of applying `a` to each element in `s` and then applying `g`.
|
pi_eq_sum_univ
theorem pi_eq_sum_univ :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {R : Type u_2} [inst_2 : Semiring R] (x : ι → R),
x = Finset.univ.sum fun i => x i • fun j => if i = j then 1 else 0
The theorem `pi_eq_sum_univ` states that for any finite type `ι`, any semiring `R` and any function `x : ι → R`, we can represent `x` as a sum over the universal finite set of `ι`. More precisely, `x` can be expressed as a sum where each term is the product of `x i` (the image of `i` under `x`) and a function that maps `j` to `1` if `i = j` and `0` otherwise. This essentially decomposes `x` as a sum along the canonical basis, and relies on the ability to decide equality in `ι`.
More concisely: For any finite type `ι`, semiring `R`, and function `x : ι → R`, there exists an element in `R` representable as a sum, where each term is the product of `x i` and a characteristic function of `{j : ι | i = j}`.
|