Sigma.vadd_mk
theorem Sigma.vadd_mk :
∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] (a : M) (i : ι) (b : α i),
a +ᵥ ⟨i, b⟩ = ⟨i, a +ᵥ b⟩
This theorem, `Sigma.vadd_mk`, states that for all types `ι`, `M`, and `α`, where `α` is a function from `ι` to some Type `u_4`, and for each `i : ι` there is a vector addition operation `VAdd M (α i)`, the addition operation on a sigma type (a dependent pair) can be decomposed. Specifically, for any `a : M`, `i : ι`, and `b : α i`, adding `a` to the sigma type with first element `i` and second element `b` results in a new sigma type with the same first element `i` and second element being `a` added to `b`.
More concisely: For all types `ι`, `M`, and functions `α : ι → u_4`, and for all `i : ι` and `a : M` and `b : (α i)`, the sigma type `Σ i, α i => a + b` is equal to the sigma type `Σ i, α i => a + π i` where `π : Σ i, α i => α i` is the projection function.
|
Sigma.smul_mk
theorem Sigma.smul_mk :
∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι) (b : α i),
a • ⟨i, b⟩ = ⟨i, a • b⟩
This theorem states that for any given types `ι`, `M` and a type dependent function `α : ι → Type`, where each `α i` is a module over `M` for all `i : ι`, the scalar multiplication `•` distributes over the creation of a sigma type, `{ fst := i, snd := b }`, which is a pair consisting of an element `i` from `ι` and an element `b` from `α i`. Specifically, multiplying `a : M` with a sigma type constructed with `i : ι` and `b : α i` is the same as creating a sigma type with `i : ι` and `a • b : α i`.
More concisely: For any type `ι`, module `M` over `ι`, and type-dependent function `α : ι → Type` such that each `α i` is an `M`-module, the scalar multiplication `• : M × α i → α i` distributes over the formation of sigma types: `a • {i : ι, b : α i} = {i : ι, a • b : α i}`.
|
Sigma.FaithfulSMul'
theorem Sigma.FaithfulSMul' :
∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] (i : ι)
[inst_1 : FaithfulSMul M (α i)], FaithfulSMul M ((i : ι) × α i)
This theorem, `Sigma.FaithfulSMul'`, states that for any types `ι`, `M`, and a type function `α` from `ι` to another type, if for every `i` of type `ι`, there is a scalar multiplication (`SMul`) operation from `M` to `α i`, and for a specific `i` the scalar multiplication is faithful (meaning different scalars produce different results when multiplied with a non-zero vector), then the scalar multiplication operation is also faithful for the type pair consisting of `ι` and `α i`.
More concisely: If for each `i` in `ι`, there exists a faithful scalar multiplication operation from `M` to `α i`, then the scalar multiplication operation from `M` to the type `α ι` is faithful.
|
Sigma.FaithfulVAdd'
theorem Sigma.FaithfulVAdd' :
∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] (i : ι)
[inst_1 : FaithfulVAdd M (α i)], FaithfulVAdd M ((i : ι) × α i)
This theorem states that, given any types `ι`, `M`, and `α` (which is a type dependent on `ι`), and given any index `i` of type `ι`, if for every `i` there's a Vector Addition structure over `M` and `α i` and if `α i` is a Faithful Vector Additive type over `M`, then the type of pairs `(i : ι) × α i` is also a Faithful Vector Additive type over `M`. In mathematical terms, it's saying that if the elements of a family of types are each endowed with a certain structure (here, faithful vector addition), then the entire family, viewed as a disjoint union (or Sigma type), also inherits that structure.
More concisely: If each type `α i` in a family indexed by `ι` is a faithful vector additive type over `M` and has a vector addition structure, then the product type `ι × Σ i, α i` is also a faithful vector additive type over `M`.
|