LinearMap.ext₂
theorem LinearMap.ext₂ :
∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] {R₂ : Type u_3} [inst_2 : Semiring R₂]
{S₂ : Type u_4} [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [inst_4 : AddCommMonoid M]
[inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
[inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
{f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}, (∀ (m : M) (n : N), (f m) n = (g m) n) → f = g
This theorem, called `LinearMap.ext₂`, states that given two semirings `R` and `S`, another two semirings `R₂` and `S₂`, and three additive commutative monoids `M`, `N`, and `P` with `M` being a module over `R`, `N` being a module over `S`, and `P` being a module over both `R₂` and `S₂`, along with the condition that scalar multiplication in `P` commutes with multiplication in `S₂` and `R₂`, if we have two linear maps `f` and `g` from `M` to `N` to `P` (i.e., each of `f` and `g` takes an element of `M` to a linear map from `N` to `P`), and if for all elements `m` in `M` and `n` in `N` the result of applying `f` and then `n` to `m` is equal to the result of applying `g` and then `n` to `m`, then `f` and `g` are equal.
More concisely: Given semirings R, S, R₂, S₂, additive commutative monoids M (an R-module), N (an S-module), and P (an (R₂, S₂)-module) with commuting scalar multiplications, if linear maps f and g from M to N to P satisfy f(m)(n) = g(m)(n) for all m in M and n in N, then f = g.
|
LinearMap.BilinForm.proof_1
theorem LinearMap.BilinForm.proof_1 : ∀ (R : Type u_1) [inst : CommSemiring R], SMulCommClass R R R
This theorem states that for any type `R` with a commutative semiring structure, the scalar multiplication of `R` is commutative. In other words, for any scalars `a`, `b` and any vector `v` in `R`, the operation `a * (b * v)` equals to `(a * b) * v`. This is one of the properties that define a commutative semiring in mathematical terms.
More concisely: For any commutative semiring `R`, the scalar multiplication is commutative, i.e., `a * (b * v) = (a * b) * v` for all scalars `a`, `b` and vectors `v` in `R`.
|
LinearMap.map_smul₂
theorem LinearMap.map_smul₂ :
∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] {S₂ : Type u_4} [inst_2 : Semiring S₂]
{M₂ : Type u_8} {N₂ : Type u_9} {P₂ : Type u_10} [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid N₂]
[inst_5 : AddCommMonoid P₂] [inst_6 : Module R M₂] [inst_7 : Module S N₂] [inst_8 : Module R P₂]
[inst_9 : Module S₂ P₂] [inst_10 : SMulCommClass S₂ R P₂] {σ₁₂ : S →+* S₂} (f : M₂ →ₗ[R] N₂ →ₛₗ[σ₁₂] P₂) (r : R)
(x : M₂) (y : N₂), (f (r • x)) y = r • (f x) y
This theorem, named `LinearMap.map_smul₂`, states that for any semirings `R`, `S`, and `S₂`, types `M₂`, `N₂`, and `P₂` that are additively commutative monoids and modules over `R`, `S`, or `S₂` respectively, and a smul commutative class of `S₂`, `R` and `P₂`, given a certain linear map `f` from `M₂` to a function from `N₂` to `P₂`, a scalar `r` from `R`, and elements `x` from `M₂` and `y` from `N₂`, the result of applying `f` to the scalar multiplication of `r` and `x` and then applying the result to `y` is equal to the scalar multiplication of `r` and the result of applying `f` to `x` and then applying the result to `y`. This is essentially a property of linear maps related to scalar multiplication.
More concisely: For linear maps `f` from an additively commutative monoid `M₂` to the function space from an additively commutative monoid `N₂` to a module `P₂` over a semiring `R`, and for any scalars `r` in `R` and elements `x` in `M₂` and `y` in `N₂`, the law of scalar multiplication holds: `f(rx)(y) = r(fx)(y)`.
|