Pi.faithfulVAdd_at
theorem Pi.faithfulVAdd_at :
∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → VAdd α (f i)] [inst_1 : ∀ (i : I), Nonempty (f i)]
(i : I) [inst_2 : FaithfulVAdd α (f i)], FaithfulVAdd α ((i : I) → f i)
This theorem states that if an indexed family of types `(f i)` has a faithful additive action with respect to a type `α` at a specific index `i`, then the entire function space `(i : I) → f i` also has a faithful additive action with respect to `α`. Here, a "faithful additive action" means that no two distinct elements of `α` act the same on any element of `f i`. Note that the index `i` cannot be automatically inferred, so it should be explicitly provided as an argument to the theorem.
More concisely: If each element in an indexed family of types `(f i)` (for `i` in `I`) has a faithful additive action with respect to type `α`, then the function space `(i : I) → f i` also has a faithful additive action with respect to `α`.
|
Pi.smul_apply'
theorem Pi.smul_apply' :
∀ {I : Type u} {f : I → Type v} (i : I) {g : I → Type u_1} [inst : (i : I) → SMul (f i) (g i)] (s : (i : I) → f i)
(x : (i : I) → g i), (s • x) i = s i • x i
This theorem, `Pi.smul_apply'`, states that for any indexed type `I`, any two functions `f : I → Type v` and `g : I → Type u_1`, any index `i : I`, and given instances of scalar multiplication (`SMul`) for each index in `I` for the types `f i` and `g i`, if we take two functions `s : (i : I) → f i` and `x : (i : I) → g i` and perform scalar multiplication on them, the result at index `i` would be the same as if we multiplied the values at index `i` of `s` and `x` directly. In other words, this theorem ensures that scalar multiplication distributes over the elements of indexed functions.
More concisely: For any indexed types I, given functions f : I -> Type and g : I -> Type, index i : I, and instances of scalar multiplication on f i and g i, we have (s smul x).i = s.i smul x.i, where s and x are functions s : i -> f i and x : i -> g i respectively.
|
Pi.single_smul'
theorem Pi.single_smul' :
∀ {I : Type u} {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : AddMonoid β]
[inst_2 : DistribMulAction α β] [inst_3 : DecidableEq I] (i : I) (r : α) (x : β),
Pi.single i (r • x) = r • Pi.single i x
This theorem, `Pi.single_smul'`, is a version of `Pi.single_smul` but for non-dependent functions. It states that for any types `I`, `α`, and `β`, where `α` has a monoid structure, `β` has an addmonoid structure, and there is a distributive multiplication action of `α` on `β`, given a decidability of equality on `I`, an element `i` of type `I`, an element `r` of type `α`, and an element `x` of type `β`, the single function at `i` with value `r • x` (the scalar multiplication of `r` and `x`) is equal to `r` scalar-multiplied by the single function at `i` with value `x`. In other words, scalar multiplication can be distributed over the single function.
More concisely: For any types `I`, `α` (monoid with distributive action on `β`), and `β` (addmonoid), given decidable equality on `I`, the single function at `i` with value `r • x` equals `r` scalar-multiplied by the single function at `i` with value `x`.
|
Pi.faithfulSMul_at
theorem Pi.faithfulSMul_at :
∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → SMul α (f i)] [inst_1 : ∀ (i : I), Nonempty (f i)]
(i : I) [inst_2 : FaithfulSMul α (f i)], FaithfulSMul α ((i : I) → f i)
The theorem `Pi.faithfulSMul_at` states that for any type `I`, a function `f` mapping `I` to another type, and a type `α`, if for a given `i` in `I`, the function `f i` has a faithful scalar action (represented by the `FaithfulSMul` structure), then the function `Π i, f i` (which is a product of `f i` over all `i` in `I`) also has a faithful scalar action. The theorem isn't an instance since the particular `i` can't be inferred. A faithful scalar action is a scalar multiplication that is injective.
More concisely: If each element in a function's image has a faithful scalar multiplication action, then the product of those images also has a faithful scalar multiplication action.
|