Module.zero_smul
theorem Module.zero_smul :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [self : Module R M] (x : M), 0 • x = 0
This theorem states that for any type `R` which forms a semiring (a structure with two associative binary operations, where one operation distributes over the other and has an identity element), and for any type `M` which forms an additive commutative monoid (a structure with an associative binary operation and an identity element, where the operation is commutative), if `R` and `M` together form a module (a structure similar to a vector space, where the scalar multiplication obeys certain rules), then the scalar multiplication of any element `x` in `M` by the zero element in `R` (denoted as `0 • x`) is equal to the zero element in `M`. Essentially, it's saying that multiplying anything by zero in this context gives zero.
More concisely: For any semiring `R` and additive commutative monoid `M` forming an `R`-module, the scalar multiplication `0 • x` equals the zero element in `M` for all `x` in `M`, where `0` denotes the zero element in `R`.
|
Module.add_smul
theorem Module.add_smul :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [self : Module R M] (r s : R) (x : M),
(r + s) • x = r • x + s • x
This theorem, `Module.add_smul`, states that for any semiring `R`, add commutative monoid `M`, and module `self` with scalar multiplication from `R` to `M`, scalar multiplication distributes over addition from the right. In other words, for any two elements `r` and `s` from the semiring `R` and any element `x` from the monoid `M`, the scalar multiplication of the sum of `r` and `s` with `x` is equal to the sum of the scalar multiplication of `r` with `x` and `s` with `x`. This is expressed in Lean 4 as `(r + s) • x = r • x + s • x`, which mirrors the standard mathematical notation.
More concisely: For any semiring R, add commutative monoid M, and module self over R with scalar multiplication, for all r, s in R and x in M, we have r • (x + s) = r • x + r • s.
|
neg_smul
theorem neg_smul :
∀ {R : Type u_2} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R) (x : M),
-r • x = -(r • x)
This theorem states that for any ring `R`, additively commutative group `M`, and a module `M` over `R`, the operation of negating a scalar multiple of a module element is the same as multiplying the module element by the negation of the scalar. In other words, if `r` is an element of `R` and `x` is an element of `M`, then the negative of `r` scalar multiplied by `x` equals the negative of (`r` scalar multiplied by `x`). This is a property of scalar multiplication in the context of ring and module theory.
More concisely: For any ring `R`, additively commutative group `M`, and `r` in `R` and `x` in `M`, $-(rx) = r\cdot(-x)$.
|
add_smul
theorem add_smul :
∀ {R : Type u_2} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r s : R)
(x : M), (r + s) • x = r • x + s • x
This theorem, named `add_smul`, is a property of scalar multiplication in the context of modules over semirings. For any given types `R` and `M`, where `R` is a semiring and `M` is an additive commutative monoid and also a module over `R`, this theorem states that for any two elements `r` and `s` from `R` and an element `x` from `M`, the scalar multiplication of the sum of `r` and `s` with `x` is equal to the sum of the scalar multiplications of `r` and `s` with `x` individually. That is, `(r + s) • x = r • x + s • x`. This is a fundamental distributive law in the theory of modules.
More concisely: For any semiring `R`, additive commutative monoid and `R`-module `M`, and elements `r`, `s` in `R` and `x` in `M`, the scalar multiplication distributes over addition: `(r + s) • x = r • x + s • x`.
|
NoZeroSMulDivisors.eq_zero_or_eq_zero_of_smul_eq_zero
theorem NoZeroSMulDivisors.eq_zero_or_eq_zero_of_smul_eq_zero :
∀ {R : Type u_9} {M : Type u_10} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMul R M]
[self : NoZeroSMulDivisors R M] {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0
This theorem, named `NoZeroSMulDivisors.eq_zero_or_eq_zero_of_smul_eq_zero`, establishes that in a setting where scalar multiplication is defined and both scalar and vector have a concept of zero, if the result of scalar multiplication is zero, then either the scalar or the vector must have been zero. In other words, it rules out the possibility of non-zero scalar and vector yielding a zero result through scalar multiplication. Here, `R` is the type of the scalar, `M` is the type of the vector, `c` is a specific scalar, and `x` is a specific vector. The theorem is applicable to any scalar and vector of the appropriate types.
More concisely: If the scalar multiplication of a non-zero scalar and a vector results in the zero vector, then the scalar or the vector must be the zero element of their respective types.
|
invOf_two_smul_add_invOf_two_smul
theorem invOf_two_smul_add_invOf_two_smul :
∀ (R : Type u_2) {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : Invertible 2] (x : M), ⅟2 • x + ⅟2 • x = x
This theorem states that for any semiring `R` and any commutative monoid `M` that also respects the scalar multiplication (thus forming a module), if 2 is invertible in `R`, then the sum of one-half of any element `x` in `M` with itself is equal to `x`. In more mathematical terms, it states that for any `x` in `M`, `½x + ½x = x`. This confirms the distributive law for scalar multiplication in the context of modules.
More concisely: For any semiring `R` and commutative monoid `M` forming an `R`-module with invertible 2, the element `½x` satisfies `½x + ½x = x` for all `x` in `M`.
|
int_smul_eq_zsmul
theorem int_smul_eq_zsmul :
∀ {M : Type u_5} [inst : AddCommGroup M] (h : Module ℤ M) (n : ℤ) (x : M), SMul.smul n x = n • x
This theorem establishes that for any integer (`ℤ`), and any element from an additive commutative group (`AddCommGroup`), the two different ways of defining scalar multiplication (`•`), one by SMul's `smul` function and the other by the canonical instance, will yield the same result. This theorem should normally not be required because by design, all additive commutative groups in the mathlib library are supposed to have exactly one `ℤ`-module structure. So, in essence, it's a safeguard against any alternative definitions of scalar multiplication, asserting that they must coincide with the standard definition.
More concisely: For any additive commutative group and integer, scalar multiplication by that integer defined using the `smul` function and the canonical instance yield the same result.
|
nat_smul_eq_nsmul
theorem nat_smul_eq_nsmul :
∀ {M : Type u_5} [inst : AddCommMonoid M] (h : Module ℕ M) (n : ℕ) (x : M), SMul.smul n x = n • x
This theorem, `nat_smul_eq_nsmul`, asserts that for any natural number `n` and any element `x` of a commutative additive monoid `M`, the action of `n` on `x` according to any exotic `ℕ`-module structure is identical to the canonical `ℕ`-module structure where `n • x` is defined by repeated addition. Here, an "exotic `ℕ`-module structure" refers to any potential alternative structure for scalar multiplication where the scalar is a natural number. Typically, however, the mathlib library is designed such that all commutative additive monoids should have exactly one `ℕ`-module structure, so this conversion should rarely, if ever, be needed.
More concisely: For any commutative additive monoid M and natural number n, the action of n on any element x in M according to any exotic ℕ-module structure equals the canonical ℕ-module structure where n • x is defined as the sum of x added to itself n times.
|
CharZero.of_noZeroSMulDivisors
theorem CharZero.of_noZeroSMulDivisors :
∀ (R : Type u_2) (M : Type u_5) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Nontrivial M] [inst_4 : NoZeroSMulDivisors ℤ M], CharZero R
This theorem states that for any ring `R` and any non-trivial module `M` over `R`, if `M` does not have any zero scalar multiplication divisors (meaning there are no non-zero scalars and non-zero module members whose scalar multiplication results in the zero module member), then `R` must have characteristic zero. In other words, only a ring of characteristic zero can have a non-trivial module without additive or scalar torsion.
More concisely: If a ring `R` has a non-trivial `R`-module `M` without scalar torsion, then `R` has characteristic zero.
|
smul_right_injective
theorem smul_right_injective :
∀ {R : Type u_2} (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] {c : R}, c ≠ 0 → Function.Injective fun x => c • x
The theorem `smul_right_injective` states that, for any semiring `R`, additive commutative group `M`, and module `M` over `R` that does not permit zero scalar multiplication with divisors, given any non-zero element `c` in `R`, the function that maps each element `x` in `M` to the scalar multiple `c • x` is injective. In other words, if `c • x = c • y` then it must be that `x = y`. This function being injective means that different elements in `M` will not be mapped to the same result under scalar multiplication by `c`.
More concisely: For any semiring R, additive commutative group M with no zero scalar multiplication by divisors of a non-zero element c in R, the function mapping x in M to c • x is injective.
|
smul_eq_zero
theorem smul_eq_zero :
∀ {R : Type u_2} {M : Type u_5} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M]
[inst_3 : NoZeroSMulDivisors R M] {c : R} {x : M}, c • x = 0 ↔ c = 0 ∨ x = 0
The theorem `smul_eq_zero` states that for any types `R` and `M`, where `R` is a zero element type and `M` is also a zero element type, and `R` and `M` have scalar multiplication with zero, and there are no zero scalar multiplication divisors in `R` and `M`, if we have a scalar `c` of type `R` and a vector `x` of type `M`, then the scalar multiplication of `c` and `x` equals zero if and only if `c` equals zero or `x` equals zero. In other words, it provides a condition for scalar multiplication to result in a zero element in the context of scalar multiplication with zero.
More concisely: For types `R` and `M` with scalar multiplication by zero and no zero divisors, the scalar multiplication of a zero scalar `c` in `R` and a vector `x` in `M` equals zero if and only if both `c` and `x` are zero.
|
Function.Injective.noZeroSMulDivisors
theorem Function.Injective.noZeroSMulDivisors :
∀ {R : Type u_9} {M : Type u_10} {N : Type u_11} [inst : Zero R] [inst_1 : Zero M] [inst_2 : Zero N]
[inst_3 : SMul R M] [inst_4 : SMul R N] [inst_5 : NoZeroSMulDivisors R N] (f : M → N),
Function.Injective f → f 0 = 0 → (∀ (c : R) (x : M), f (c • x) = c • f x) → NoZeroSMulDivisors R M
The theorem `Function.Injective.noZeroSMulDivisors` states that, given two types `R` and `M` and another type `N`, along with instances of `Zero R`, `Zero M`, `Zero N`, `SMul R M`, `SMul R N`, and `NoZeroSMulDivisors R N`, and given an injective function `f` from `M` to `N` that maps zero in `M` to zero in `N` and preserves scalar multiplication (i.e., for all scalar `c` in `R` and all `x` in `M`, `f` applied to `c` scalar multiplied by `x` equals `c` scalar multiplied by `f` applied to `x`), then `M` has the property `NoZeroSMulDivisors R M`.
In other words, if scalar multiplication by a non-zero element in `R` results in zero in `N`, then either the scalar was zero or the original element in `M` was zero, under the condition that `f` is injective and preserves scalar multiplication. This theorem allows the property of having no zero scalar multiplication divisors to be pulled back along an injective function from `M` to `N`.
More concisely: If `f` is an injective function from `M` to `N` that maps zero in `M` to zero in `N` and preserves scalar multiplication, then `M` has no zero scalar multiplication divisors if and only if `N` has no zero scalar multiplication divisors.
|
Module.subsingleton
theorem Module.subsingleton :
∀ (R : Type u_9) (M : Type u_10) [inst : Semiring R] [inst_1 : Subsingleton R] [inst_2 : AddCommMonoid M]
[inst : Module R M], Subsingleton M
This theorem states that if we have a module `M` over a semiring `R` and `R` is a `Subsingleton`, then `M` is also a `Subsingleton`. In other words, if there's only one unique element in the semiring `R`, then there can only be one unique element in the module `M` as well. However, this cannot be registered as an instance since Lean cannot guess `R`.
More concisely: If `R` is a subsingleton semiring, then the module `M` over `R` has at most one element.
|
two_smul
theorem two_smul :
∀ (R : Type u_2) {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
2 • x = x + x
This theorem, `two_smul`, states that for any type `R`, and any commutative additive monoid `M` that is also a module over `R`, the scalar multiplication of `2` and any element `x` of `M` is equal to the sum of `x` with itself. This is a general principle of scalar multiplication in algebraic structures, where scaling by `2` is the same as adding the element to itself. Here, `Semiring R` implies that `R` is a semiring and `Module R M` implies that `M` is a module over `R`.
More concisely: For any commutative additive monoid `M` that is a module over a semiring `R`, the scalar multiplication of `2` and any element `x` in `M` equals the sum `x + x`.
|
sub_smul
theorem sub_smul :
∀ {R : Type u_2} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r s : R) (y : M),
(r - s) • y = r • y - s • y
This theorem states that for any ring `R` and any additive commutative group `M` that forms a module over `R`, the operation of scalar multiplication distributes over subtraction. Specifically, for any two scalars `r` and `s` from `R` and any vector `y` from `M`, the scalar multiplication of the difference of `r` and `s` with `y` equals to the difference of the scalar multiplication of `r` with `y` and the scalar multiplication of `s` with `y`. This property is written in LaTeX as: `(r - s) • y = r • y - s • y`.
More concisely: For any ring `R`, additive commutative group `M` (an `R`-module), scalars `r, s ∈ R`, and vector `y ∈ M`, we have `(r - s) • y = r • y - s • y`.
|
self_eq_neg
theorem self_eq_neg :
∀ (R : Type u_2) (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] [inst : CharZero R] {v : M}, v = -v ↔ v = 0
This theorem is named `self_eq_neg` and states that for any semiring `R`, any additive commutative group `M`, and any module `M` over `R`, given the conditions that there are no zero scalar multipliers or divisors in `R` and `M`, and `R` has characteristic zero, a vector `v` in `M` is equal to its own negation if and only if `v` is the zero vector. In mathematical notation, this can be represented as `∀v ∈ M, v = -v ↔ v = 0`.
More concisely: For any semiring R with no zero scalar multipliers or divisors and characteristic zero, and any additive commutative group M with no zero divisors as an R-module, every vector v in M satisfies v = -v if and only if v is the zero vector.
|
neg_smul_neg
theorem neg_smul_neg :
∀ {R : Type u_2} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R) (x : M),
-r • -x = r • x
The theorem `neg_smul_neg` states that for every ring `R`, additive commutative group `M`, and module `M` over `R`, for any element `r` from `R` and any element `x` from `M`, the scalar multiplication of the negation of `r` and the negation of `x` equals the scalar multiplication of `r` and `x`. In mathematical terms, it says that for any ring `R` and any `R`-module `M`, if `r` is an element of `R` and `x` is an element of `M`, then `(-r) * (-x) = r * x`.
More concisely: For every ring `R` and `R`-module `M`, the negation of their scalar multiplication is commutative, that is, `(-r) * (-x) = r * x` for all `r` in `R` and `x` in `M`.
|
Module.nontrivial
theorem Module.nontrivial :
∀ (R : Type u_9) (M : Type u_10) [inst : Semiring R] [inst_1 : Nontrivial M] [inst_2 : AddCommMonoid M]
[inst : Module R M], Nontrivial R
This theorem states that for any given types `R` and `M`, if `R` is a semiring, `M` is a nontrivial additive commutative monoid, and `M` is a module over `R`, then `R` is a nontrivial semiring. Here, a semiring is called nontrivial if it contains at least two distinct elements. This is established by the existence of a nontrivial module `M` over the semiring `R`.
More concisely: If `R` is a semiring, `M` is a nontrivial additive commutative monoid that is an `R`-module, then `R` is a nontrivial semiring.
|
smul_left_injective
theorem smul_left_injective :
∀ (R : Type u_2) {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] {x : M}, x ≠ 0 → Function.Injective fun c => c • x
The theorem `smul_left_injective` states that for any ring `R`, additive commutative group `M`, and module `M` over `R`, given the condition that there are no zero scalar multipliers and divisors in `R` and `M`, if a non-zero element `x` from `M` is given, then the function that maps each element `c` from `R` to the result of the scalar multiplication of `c` and `x` is injective. In other words, scalar multiplication by a non-zero element is an injective function: if `c1` and `c2` are two elements from `R` such that `c1 • x = c2 • x`, then `c1` must be equal to `c2`.
More concisely: If `R` is a ring with no zero divisors, and `M` is an `R`-module with no zero scalar multipliers, then scalar multiplication by a non-zero element `x` in `M` is injective.
|
Units.neg_smul
theorem Units.neg_smul :
∀ {R : Type u_2} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (u : Rˣ) (x : M),
-u • x = -(u • x)
This theorem states that for any ring `R`, additive commutative group `M`, and `M` being a module over `R`, the negation of the scalar multiplication of a unit `u` in `R` and an element `x` in `M` is equal to the scalar multiplication of `u` and `x` followed by negation. In mathematical terms, `-u • x = -(u • x)`.
More concisely: For any ring `R` with unity, module `M` over `R`, and `u` a unit in `R` and `x` an element in `M`, we have `-u * x = -(u * x)`.
|
neg_one_smul
theorem neg_one_smul :
∀ (R : Type u_2) {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : M),
-1 • x = -x
This theorem, `neg_one_smul`, states that for any given type `R` that is a ring, and any given type `M` that is an additively commutative group and also a module over `R`, the scalar multiplication of `-1` and any element `x` of type `M` is equal to the negation of `x`. In other words, multiplying any element of the module by `-1` results in the additive inverse of that element.
More concisely: For any ring `R` and additively commutative group `M` being an `R`-module, for all `x` in `M`, `-1 * x = -x`.
|
Convex.combo_self
theorem Convex.combo_self :
∀ {R : Type u_2} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {a b : R},
a + b = 1 → ∀ (x : M), a • x + b • x = x
The theorem `Convex.combo_self` states that for any semiring `R`, any additive commutative monoid `M`, and any module `M` over `R`, if `a` and `b` are elements of `R` such that `a + b` is equal to `1`, then for any `x` in `M`, the sum of `a` scaled by `x` and `b` scaled by `x` equals `x`. In other words, this theorem describes a property of convex combinations in the context of linear algebra, stating that if a point `x` is expressed as a convex combination of itself, then the coefficients add up to 1.
More concisely: For any semiring R, additive commutative monoid M, and R-module M, if a and b are elements of R with a + b = 1, then for any x in M, ax + bx = x.
|
CharZero.of_module
theorem CharZero.of_module :
∀ (R : Type u_2) [inst : Semiring R] (M : Type u_9) [inst_1 : AddCommMonoidWithOne M] [inst_2 : CharZero M]
[inst_3 : Module R M], CharZero R
This theorem states that if we have a module `M` over a semiring `R` such that `M` has a multiplicative identity (one) and has characteristic zero, then the semiring `R` must also have characteristic zero. Here, the concept of a 'characteristic' of a ring or module refers to the smallest positive integer `n` such that `n*a = 0` for all elements `a` in the ring or module. If no such `n` exists, the characteristic is said to be zero. Often, `M` is an `R`-algebra.
More concisely: If `M` is a module of characteristic zero over a semiring `R` with a multiplicative identity, then `R` also has characteristic zero.
|
zsmul_eq_smul_cast
theorem zsmul_eq_smul_cast :
∀ (R : Type u_2) {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℤ) (b : M),
n • b = ↑n • b
This theorem states that for any ring `R`, any additive commutative group `M`, any module `M` over the ring `R`, any integer `n` and any element `b` of `M`, the scaled multiple of `b` by `n` in the context of integer multiples (`n • b`) is equal to the scaled multiple of `b` by the casting of `n` to a ring element (`↑n • b`). This essentially formalizes the notion that scaling by an integer in a module context is the same as scaling by that integer treated as a ring element.
More concisely: For any ring `R`, additive commutative group `M`, module `M` over `R`, integer `n`, and element `b` of `M`, `n • b` = ↑n • b`.
|
Module.ext'
theorem Module.ext' :
∀ {R : Type u_9} [inst : Semiring R] {M : Type u_10} [inst_1 : AddCommMonoid M] (P Q : Module R M),
(∀ (r : R) (m : M), r • m = r • m) → P = Q
This theorem, referred to as `Module.ext'`, states that for any semiring `R` and any additive commutative monoid `M`, if two `Module` structures `P` and `Q` over `R` and `M` have the same scalar multiplication operation (denoted by `•`), then `P` and `Q` are equal. In simpler words, if two modules over the same semiring and the same base set behave the same way under scalar multiplication, then they are indeed the same module.
More concisely: If two `Module` structures over the same semiring and additive commutative monoid have identical scalar multiplication operations, then they represent the same module.
|
nsmul_eq_smul_cast
theorem nsmul_eq_smul_cast :
∀ (R : Type u_2) {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ)
(b : M), n • b = ↑n • b
The theorem `nsmul_eq_smul_cast` states that for any semiring `R`, any additive commutative monoid `M`, and any `R`-module structure on `M`, the operation of scalar multiplication by a natural number `n` on an element `b` of `M` (`n • b`) is equal to the action of `n` cast to `R` acting on `b` (`↑n • b`). This essentially says that scalar multiplication by a natural number in the module is the same as multiplying by that number viewed as an element of the semiring.
More concisely: For any semiring R, additive commutative monoid M with an R-module structure, and natural number n, the operation n • b of scalar multiplication on M equals the operation (↑n • b) obtained by casting n to R and acting on b.
|
Nat.smul_one_eq_coe
theorem Nat.smul_one_eq_coe : ∀ {R : Type u_9} [inst : Semiring R] (m : ℕ), m • 1 = ↑m
This theorem states that for any natural number `m` and any semiring `R`, the result of scaling (`smul`) the number `1` by `m` is equivalent to the coersion of `m` into `R`. Essentially, it emphasizes that in the context of semirings, multiplying `1` by any natural number `m` yields the same value as if `m` was simply converted into the type of the semiring.
More concisely: For any semiring R and natural number m, 1 × m = R.coerce m.
|