map_rat_smul
theorem map_rat_smul :
∀ {M : Type u_3} {M₂ : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] [_instM : Module ℚ M]
[_instM₂ : Module ℚ M₂] {F : Type u_5} [inst_2 : FunLike F M M₂] [inst_3 : AddMonoidHomClass F M M₂] (f : F)
(c : ℚ) (x : M), f (c • x) = c • f x
The theorem `map_rat_smul` states that for any rational number `c`, any element `x` of a module `M` over the rational numbers, and any function `f` that is an additively commutative group homomorphism from `M` to another module `M₂` over the rational numbers, the result of applying `f` to the result of scaling `x` by `c` (`f (c • x)`) is the same as the result of scaling the result of applying `f` to `x` by `c` (`c • f x`). This property holds for all types `M`, `M₂`, and `F` where `M` and `M₂` are additively commutative groups and `F` is a function type such that functions of type `F` can be treated as functions from `M` to `M₂`, and `F` forms an additively commutative group homomorphism class from `M` to `M₂`.
More concisely: For any additively commutative group homomorphism `f` and rational number `c`, the application of `f` to the scalar multiplication `c • x` of an element `x` in an additively commutative group `M` is equal to the scalar multiplication `c • f x` of the image `f x` in another additively commutative group `M₂`.
|
Mathlib.Algebra.Module.Basic._auxLemma.4
theorem Mathlib.Algebra.Module.Basic._auxLemma.4 : ∀ (p : Prop), (False ∨ p) = p
This theorem, `Mathlib.Algebra.Module.Basic._auxLemma.4`, states that for any types `R` and `M`, given that `R` has a zero and `M` also has a zero, and given that scalar multiplication with zero in `R` on `M` is defined and there exists no zero scalar multiplication divisors in `R` and `M`, then for any elements `c` from `R` and `x` from `M`, the equality `c` times `x` equals zero holds if and only if either `c` equals zero or `x` equals zero. This is a fundamental property in algebra where the product of two elements is zero if and only if one or both of the elements are zero.
More concisely: For any commutative ring `R` with identity and any additive abelian group `M`, if scalar multiplication by zero in `R` on `M` is zero and there are no zero divisors for scalars or vectors, then the product of an element from `R` and an element from `M` is zero if and only if one of them is zero.
|
Function.support_smul_subset_right
theorem Function.support_smul_subset_right :
∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : SMulZeroClass R M] (f : α → R) (g : α → M),
Function.support (f • g) ⊆ Function.support g
The theorem `Function.support_smul_subset_right` states that for any two functions `f : α → R` and `g : α → M`, where `R` is a scalar multiplication zero class and `M` has a zero element, the support (set of points where the function is non-zero) of the scalar multiplication of `f` and `g` (represented as `f • g`) is a subset of the support of the function `g`. In other words, any element in the domain `α` for which `f • g` is non-zero must also be an element for which `g` is non-zero.
More concisely: The support of the scalar multiplication of two functions `f : α → R` and `g : α → M` is contained in the support of `g`, where `R` is a scalar multiplication zero class and `M` has a zero element. In other words, for all `x ∈ α`, if `f • g(x) ≠ 0`, then `g(x) ≠ 0`.
|
Function.support_smul_subset_left
theorem Function.support_smul_subset_left :
∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M]
(f : α → R) (g : α → M), Function.support (f • g) ⊆ Function.support f
The theorem `Function.support_smul_subset_left` states that for any types `α`, `R`, and `M`, where `R` and `M` have zero elements and `R` and `M` have a scalar multiplication operation compatible with zero, and any functions `f : α → R` and `g : α → M`, the support of the scalar multiplication of `f` and `g` (i.e., the set of points where `f(x) * g(x)` is non-zero) is a subset of the support of `f` (i.e., the set of points where `f(x)` is non-zero). Essentially, this means that if a point is in the support of the multiplied functions, it must be in the support of the first function `f`.
More concisely: For functions `f : α → R` and `g : α → M` between types with zero elements and scalar multiplication, the support of their product `f * g` is contained in the support of `f`.
|