Module.End.intCast_apply
theorem Module.End.intCast_apply :
∀ {R : Type u_1} {N₁ : Type u_10} [inst : Semiring R] [inst_1 : AddCommGroup N₁] [inst_2 : Module R N₁] (z : ℤ)
(m : N₁), ↑z m = z • m
This theorem, `Module.End.intCast_apply`, states that for any semiring `R`, any additive commutative group `N₁`, and any `R`-module `N₁`, for any integer `z` and any element `m` of `N₁`, casting `z` to the endomorphisms of `N₁` and then applying this endomorphism to `m` is the same as scaling `m` by `z` in the `R`-module `N₁`. In terms of mathematical notation, it states that for all `z ∈ ℤ` and `m ∈ N₁`, `↑z m = z • m`.
More concisely: For any semiring R, additive commutative group N₁, and R-module structure on N₁, casting an integer z to the endomorphisms of N₁ and applying it to an element m of N₁ equals scaling m by z in the R-module N₁, that is, ↑z (m) = z • m.
|
LinearMap.mul_eq_comp
theorem LinearMap.mul_eq_comp :
∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(f g : Module.End R M), f * g = f ∘ₗ g
This theorem states that for any semiring `R` and any additive commutative monoid `M` that also has a `R`-module structure, for any two endomorphisms `f` and `g` of the `R`-module `M`, the multiplication of `f` and `g` (in the sense of the ring structure on the endomorphism ring `Module.End R M`) is equal to the linear composition of `f` and `g` (i.e., first applying `g`, then `f`). In other words, the ring multiplication on the endomorphism ring corresponds to the composition of endomorphisms.
More concisely: For any semiring `R`, additive commutative `R`-module `M`, and endomorphisms `f` and `g` of `M`, `Module.End R M.mul (f : M → M) (g : M → M) = g ∘ f`.
|
LinearMap.mul_apply
theorem LinearMap.mul_apply :
∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(f g : Module.End R M) (x : M), (f * g) x = f (g x)
The theorem `LinearMap.mul_apply` states that for any semiring `R`, any additive commutative monoid `M`, with `M` being a module over `R`, and any two endomorphisms `f` and `g` of `M` defined over `R`, the multiplication of `f` and `g` applied to an element `x` of `M` (i.e., `(f * g) x`) is equal to `f` applied to the result of `g` applied to `x` (i.e., `f (g x)`). In other words, the multiplication operation on linear endomorphisms corresponds to the composition of those endomorphisms.
More concisely: For any semiring R, additive commutative monoid M being an R-module, and endomorphisms f and g of M, we have (f * g) x = f (g x) for all x in M, i.e., multiplication of endomorphisms corresponds to their composition.
|
Module.End.natCast_apply
theorem Module.End.natCast_apply :
∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ)
(m : M), ↑n m = n • m
The theorem `Module.End.natCast_apply` states that for any semiring `R`, any add-commutative monoid `M`, and any `M` that is also a module over `R`, for any natural number `n` and any element `m` of `M`, casting `n` to an endomorphism of `M` and applying this endomorphism to `m` is the same as scaling `m` by `n` using the scalar multiplication of the module. In other words, the action of the natural number endomorphism on a module element is equivalent to scalar multiplication. It's a statement about how natural numbers interact with the scalar multiplication in a module.
More concisely: For any semiring R, add-commutative monoid M that is an R-module, and natural number n, the endomorphism of M cast from n and applied to any element m is equivalent to scaling m by n via R-module scalar multiplication.
|
LinearMap.coe_pow
theorem LinearMap.coe_pow :
∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f : M →ₗ[R] M)
(n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
This theorem states that, for any semiring `R`, an additive commutative monoid `M`, and a module structure on `M` over `R`, given a linear map `f` from `M` to `M` and a natural number `n`, the nth power of the map `f` coincides with the nth iterate of `f`. In other words, applying the linear map `f` `n` times is the same as applying the nth power of `f` once.
More concisely: For any semiring `R`, additive commutative monoid `M` with an `R`-module structure, linear map `f` from `M` to `M`, and natural number `n`, the `n`th power of `f` equals the `n` iterates of `f`: `(f ^ n) = f ^ (n-1) ∘ ... ∘ f`.
|
LinearMap.one_apply
theorem LinearMap.one_apply :
∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
1 x = x
This theorem states that for any given semiring 'R', commutative monoid 'M', and module 'M' over 'R', the application of the identity element (1) of the semiring to any element 'x' of the module is equal to 'x' itself. In simpler terms, multiplying any element by one in the context of a linear map results in the element itself.
More concisely: For any semiring R, commutative monoid M with R-module structure, and all x in M, 1 \* x = x.
|