LinearMap.stdBasis_ne
theorem LinearMap.stdBasis_ne :
∀ (R : Type u_1) {ι : Type u_2} [inst : Semiring R] (φ : ι → Type u_3) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
[inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (i j : ι),
j ≠ i → ∀ (b : φ i), (LinearMap.stdBasis R φ i) b j = 0
The theorem `LinearMap.stdBasis_ne` states that for any semiring `R`, a type function `φ` mapping from type `ι` to some types `u_3`, and any instances of the additive commutative monoid and `R`-module structures over the types `φ i` for each `i : ι`, given that the equality on type `ι` is decidable, if we take two distinct elements `i` and `j` from `ι`, then for any element `b` of type `φ i`, the value of the standard basis linear map associated to `i`, when applied to `b` and then evaluated at `j`, is zero. This theorem essentially demonstrates that the standard basis linear maps are orthogonal in the sense that different basis maps do not interfere with each other.
More concisely: For any semiring `R`, given a type function `φ : ι → u_3` with decidable equality on `ι`, and instances of the additive commutative monoid and `R`-module structures over `φ i` for all `i : ι`, the standard basis linear maps associated to distinct elements of `ι` are orthogonal, i.e., their values applied to any basis element and evaluated at another basis element are equal to zero.
|
LinearMap.stdBasis_same
theorem LinearMap.stdBasis_same :
∀ (R : Type u_1) {ι : Type u_2} [inst : Semiring R] (φ : ι → Type u_3) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
[inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (i : ι) (b : φ i),
(LinearMap.stdBasis R φ i) b i = b
The theorem "LinearMap.stdBasis_same" states that for any semi-ring `R`, index type `ι`, a family of types `φ : ι → Type`, where each `φ i` is an additively commutative monoid and a module over `R`, and a decidable equality on `ι`, given an index `i` of type `ι` and an element `b` of `φ i`, applying the standard basis linear map on `b` and then evaluating it at `i` will yield `b` itself. Essentially, it asserts that the standard basis linear map behaves as expected when applied to its corresponding index in the basis.
More concisely: For any semi-ring `R`, index type `ι`, a family of additively commutative monoids and `R`-modules `φ : ι → Type`, and a decidable equality on `ι`, the standard basis linear map on an element `b` of `φ i` evaluated at `i` equals `b` itself.
|