Mathlib.LinearAlgebra.Pi._auxLemma.1
theorem Mathlib.LinearAlgebra.Pi._auxLemma.1 :
∀ {α : Sort u_1} {β : α → Sort u} {f₁ f₂ : (x : α) → β x}, (f₁ = f₂) = ∀ (a : α), f₁ a = f₂ a
This theorem, named `_auxLemma.1` in the `LinearAlgebra.Pi` namespace of Mathlib, states that for any two functions `f₁` and `f₂` of arbitrary types `β x` over a domain `α`, the equality of these two functions is equivalent to the equality of their values at every point `a` in the domain `α`. In mathematical terms, for all functions `f₁` and `f₂` from `α` to `β x`, `f₁` is equal to `f₂` if and only if `f₁(a) = f₂(a)` for every `a` in `α`.
More concisely: For functions `f₁` and `f₂` from a domain `α` to a type `β x`, `f₁` equals `f₂` if and only if for all `a` in `α`, `f₁(a)` equals `f₂(a)`.
|
LinearMap.pi_ext'
theorem LinearMap.pi_ext' :
∀ {R : Type u} {M : Type v} {ι : Type x} [inst : Semiring R] {φ : ι → Type i}
[inst_1 : (i : ι) → AddCommMonoid (φ i)] [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : Finite ι]
[inst_4 : DecidableEq ι] [inst_5 : AddCommMonoid M] [inst_6 : Module R M] {f g : ((i : ι) → φ i) →ₗ[R] M},
(∀ (i : ι), f ∘ₗ LinearMap.single i = g ∘ₗ LinearMap.single i) → f = g
This theorem, `LinearMap.pi_ext'`, states that for any semiring `R`, Type `M`, Type index `ι`, a function `φ : ι → Type i`, and given the conditions that for each `i` in `ι`, `φ i` forms an additive commutative monoid and a module over `R`, that `ι` is finite and has decidable equality, and `M` forms an additive commutative monoid and a module over `R`, for any two linear maps `f` and `g` from the function space `(i : ι) → φ i` to `M`, if for all `i` in `ι`, the composition of `f` with the single linear map at `i` is equal to the composition of `g` with the single linear map at `i`, then `f` is equal to `g`. In simpler terms, it tells that if two linear maps agree on all single-element inputs, then they are equal.
More concisely: Given a semiring `R`, a finite index type `ι`, an additive commutative monoid `M` that is an `R`-module, and functions `f` and `g` from `ι` to `M` such that `φ i` forms an additive commutative monoid and an `R`-module for each `i`, if `f i = g i` for all `i` in `ι`, then `f = g`.
|
LinearMap.pi_apply_eq_sum_univ
theorem LinearMap.pi_apply_eq_sum_univ :
∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
[inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (f : (ι → R) →ₗ[R] M₂) (x : ι → R),
f x = Finset.univ.sum fun i => x i • f fun j => if i = j then 1 else 0
This theorem states that for any semiring `R`, an additive commutative monoid `M₂`, a module `M₂` over `R`, a finite type `ι`, and a decidable equality on `ι`, a linear map `f` from `ι → R` to `M₂`, and a function `x : ι → R`, the result of applying `f` to `x` is the sum over all `i` in the universe of the finite set `Finset.univ` of `x i` scaled by `f` applied to the function that returns `1` if `i` equals `j` and `0` otherwise. In mathematical terms, this theorem states that the result of a linear map applied to a vector can be computed as the sum of the scalar multiples of the images under the linear map of the elements of the canonical basis.
More concisely: For any semiring `R`, additive commutative monoid `M₂`, module `M₂` over `R`, finite type `ι`, decidable equality on `ι`, linear map `f` from `ι` to `M₂`, and function `x : ι → R`, the result of applying `f` to `x` is equal to the sum over all `i` in `ι` of `x i` scaled by `f i`.
|