IsScalarTower.smul_assoc
theorem IsScalarTower.smul_assoc :
∀ {M : Type u_10} {N : Type u_11} {α : Type u_12} [inst : SMul M N] [inst_1 : SMul N α] [inst_2 : SMul M α]
[self : IsScalarTower M N α] (x : M) (y : N) (z : α), (x • y) • z = x • y • z
This theorem states the associativity of the scalar multiplication operation `•`. If we have three types `M`, `N`, and `α`, where `M` is a scalar over `N`, `N` is a scalar over `α`, and `M` is also a scalar over `α`, then for any elements `x` of `M`, `y` of `N`, and `z` of `α`, the operation `(x • y) • z` is equal to `x • (y • z)`. Here, `IsScalarTower M N α` means that the scalar multiplication operations are compatible, i.e., `M`, `N`, and `α` form a scalar tower.
More concisely: For any scalar towers `M` over `N` and `N` over `α`, the associativity of scalar multiplication holds, i.e., `(x • y) • z = x • (y • z)` for all `x ∈ M`, `y ∈ N`, and `z ∈ α`.
|
MulAction.one_smul
theorem MulAction.one_smul :
∀ {α : Type u_10} {β : Type u_11} [inst : Monoid α] [self : MulAction α β] (b : β), 1 • b = b
This theorem asserts that for any types `α` and `β`, given that `α` has a monoid structure and `β` is a `MulAction` over `α`, for every element `b` of type `β`, the scalar multiplication of `1` (the identity element of the monoid `α`) and `b` equals `b` itself. In other words, `1` acts as the neutral element in the scalar multiplication operation for all elements in `β`.
More concisely: For any monoid `α` and `MulAction` `β` over `α`, the scalar multiplication of the identity element `1` in `α` with any element `b` in `β` equals `b`.
|
DistribSMul.smul_add
theorem DistribSMul.smul_add :
∀ {M : Type u_10} {A : Type u_11} [inst : AddZeroClass A] [self : DistribSMul M A] (a : M) (x y : A),
a • (x + y) = a • x + a • y
The theorem `DistribSMul.smul_add` states that for any types `M` and `A`, where `A` is an additive group with zero and `M` and `A` have a distributive scalar multiplication operation, scalar multiplication distributes over addition. In other words, given any scalar `a` of type `M` and any elements `x` and `y` of type `A`, the scalar product of `a` with the sum of `x` and `y` is equal to the sum of the scalar product of `a` with `x` and the scalar product of `a` with `y`. This is a type-generic version of the well-known algebraic property that "multiplication distributes over addition".
More concisely: For any additive group `A` with zero and type `M` having a distributive scalar multiplication with `A`, the law of distributivity of scalar multiplication over addition holds: `(a : M) * (x : A) + (a : M) * (y : A) = a * (x : A) + a * (y : A)` for all `x, y : A`.
|
Commute.smul_right
theorem Commute.smul_right :
∀ {M : Type u_1} {α : Type u_6} [inst : SMul M α] [inst_1 : Mul α] [inst_2 : SMulCommClass M α α]
[inst_3 : IsScalarTower M α α] {a b : α}, Commute a b → ∀ (r : M), Commute a (r • b)
This theorem, `Commute.smul_right`, states that for any types `M` and `α` with defined scalar multiplication and multiplication, given that the scalar multiplication commutes with the multiplication and the scalar multiplication satisfies the scalar tower property, if two elements `a` and `b` of type `α` commute (i.e., `a * b = b * a`), then for any scalar `r` of type `M`, `a` commutes with the scalar multiplication of `r` and `b` (i.e., `a * (r • b) = (r • b) * a`).
More concisely: If `α` is a type with defined scalar multiplication and multiplication, and scalar multiplication commutes with multiplication and satisfies the scalar tower property, then for all `a, b ∈ α` with `a * b = b * a`, we have `a * (r • b) = (r • b) * a` for any scalar `r ∈ M`.
|
FaithfulVAdd.eq_of_vadd_eq_vadd
theorem FaithfulVAdd.eq_of_vadd_eq_vadd :
∀ {G : Type u_10} {P : Type u_11} [inst : VAdd G P] [self : FaithfulVAdd G P] {g₁ g₂ : G},
(∀ (p : P), g₁ +ᵥ p = g₂ +ᵥ p) → g₁ = g₂
This theorem, named `FaithfulVAdd.eq_of_vadd_eq_vadd`, states that for any given types `G` and `P` with a vector addition structure (`VAdd`), if the type `P` has the property of `FaithfulVAdd` (i.e., distinct elements of `G` act differently on `P`), then whenever two elements `g₁` and `g₂` from `G` act identically on all points of type `P` (i.e., for all `p` in `P`, `g₁ +ᵥ p` equals `g₂ +ᵥ p`), it must be concluded that `g₁` and `g₂` are indeed the same (i.e., `g₁ = g₂`).
More concisely: If `G` is a type with vector addition structure and `P` is a type with the FaithfulVAdd property, then for all `g₁ g₂` in `G` and `p` in `P`, if `g₁ +ᵥ p = g₂ +ᵥ p` for all `p`, then `g₁ = g₂`.
|
zero_vadd
theorem zero_vadd : ∀ (M : Type u_1) {α : Type u_6} [inst : AddMonoid M] [inst_1 : AddAction M α] (b : α), 0 +ᵥ b = b
This theorem states that for any type `M`, and any other type `α` which is an additive action of `M`, when 0 (from the additive monoid `M`) is vector-added (`+ᵥ`) to any element `b` of the type `α`, the result is `b` itself. In mathematical terms, it's expressing that 0 acts as an identity for the vector addition operation in the context of an additive action.
More concisely: For any additive action `α` of type `M`, the additive identity 0 of `M` leaves elements of `α` unchanged under vector addition, i.e., `0 +ᵥ b = b` for all `b` in `α`.
|
smul_assoc
theorem smul_assoc :
∀ {α : Type u_6} {M : Type u_10} {N : Type u_11} [inst : SMul M N] [inst_1 : SMul N α] [inst_2 : SMul M α]
[inst_3 : IsScalarTower M N α] (x : M) (y : N) (z : α), (x • y) • z = x • y • z
This theorem, `smul_assoc`, asserts the associativity of scalar multiplication across three types `M`, `N`, and `α` in a scalar tower context. In particular, for any elements `x` of type `M`, `y` of type `N`, and `z` of type `α`, with `M` being a scalar of `N` and `N` being a scalar of `α`, the result of first performing scalar multiplication of `x` and `y`, and then taking the result to scalar multiply `z`, is the same as the result of first scalar multiplying `y` and `z`, and then letting `x` scale the result. In mathematical notation, it states that $(x \cdot y) \cdot z = x \cdot (y \cdot z)$, where $\cdot$ denotes scalar multiplication.
More concisely: For any scalars x of type M, y of type N, and z of type α, with M being a scalar of N and N being a scalar of α, the associativity of scalar multiplication holds: (x · y) · z = x · (y · z).
|
smul_neg
theorem smul_neg :
∀ {M : Type u_1} {A : Type u_4} [inst : Monoid M] [inst_1 : AddGroup A] [inst_2 : DistribMulAction M A] (r : M)
(x : A), r • -x = -(r • x)
This theorem, `smul_neg`, states that for any types `M` and `A`, where `M` is a monoid, `A` is an additive group, and `A` is also a distributive `M`-action, the scalar multiplication of a monoid element `r` and the additive inverse of an element `x` from `A` is equal to the additive inverse of the scalar multiplication of `r` and `x`. In terms of mathematical notation, this corresponds to the property `r * -x = -(r * x)`, where `*` denotes the action of `M` on `A`.
More concisely: For any monoid `M`, additive group `A`, and distributive `M`-action on `A`, the scalar multiplication of an element `r` in `M` and the additive inverse `-x` of an element `x` in `A` equals the additive inverse of the scalar multiplication of `r` and `x`, i.e., `r * -x = -(r * x)`.
|
MulDistribMulAction.smul_one
theorem MulDistribMulAction.smul_one :
∀ {M : Type u_10} {A : Type u_11} [inst : Monoid M] [inst_1 : Monoid A] [self : MulDistribMulAction M A] (r : M),
r • 1 = 1
This theorem states that for any scalars `r` of type `M` under the conditions that `M` is a monoid and `A` is a monoid with a multiplication-distributive scalar action (defined by `MulDistribMulAction M A`), the scalar multiplication of `r` with the identity element `1` yields the identity element `1`. In other words, scaling the identity by any factor in a multiplicative monoid with a distributive scalar action leaves the identity unchanged. In mathematical terms, for all `r` in `M`, `r * 1 = 1`.
More concisely: For any monoid `M` with a distributive scalar action on a monoid `A`, scaling the identity element `1` of `A` by any scalar `r` in `M` results in the identity element `1` of `A`. In other words, `r * 1 = 1` for all `r` in `M`.
|
vadd_vadd
theorem vadd_vadd :
∀ {M : Type u_1} {α : Type u_6} [inst : AddMonoid M] [inst_1 : AddAction M α] (a₁ a₂ : M) (b : α),
a₁ +ᵥ (a₂ +ᵥ b) = a₁ + a₂ +ᵥ b
This theorem states that for any underlying type `M` that forms an additive monoid, and any type `α` on which `M` acts additively, the vector addition operation respects the associativity of the monoid's addition. Specifically, for any elements `a₁`, `a₂` of `M` and `b` of `α`, the equation `a₁ +ᵥ (a₂ +ᵥ b) = a₁ + a₂ +ᵥ b` holds. Here, `+ᵥ` denotes the vector addition operation, and `+` denotes the addition operation in the monoid `M`.
The `AddAction M α` structure indicates that `M` acts on `α` in a way that respects the addition operation in `M`.
More concisely: For any additive monoid `M` and any additive action `AddAction M α`, the vector addition `+ᵥ` of elements in `M` on a type `α` is associative with respect to the monoid addition `+` of `M`, i.e., `(a₁ + a₂) +ᵥ b = a₁ +ᵥ (a₂ + b)` for all `a₁`, `a₂` in `M` and `b` in `α`.
|
FaithfulSMul.eq_of_smul_eq_smul
theorem FaithfulSMul.eq_of_smul_eq_smul :
∀ {M : Type u_10} {α : Type u_11} [inst : SMul M α] [self : FaithfulSMul M α] {m₁ m₂ : M},
(∀ (a : α), m₁ • a = m₂ • a) → m₁ = m₂
This theorem states that for any two elements 'm₁' and 'm₂' of type 'M', if they have the same action on all points of type 'α' (i.e., if for every point 'a' of type 'α', applying 'm₁' to 'a' results in the same as applying 'm₂' to 'a'), then 'm₁' and 'm₂' are equal. This holds under the condition that the scalar multiplication operation 'SMul M α' is faithful, meaning it uniquely identifies points in 'M' based on their action on points in 'α'.
More concisely: If 'M' is a vector space over a field 'α' with faithful scalar multiplication, then any two elements 'm₁' and 'm₂' in 'M' that agree on the action on all points in 'α' are equal.
|
smul_add
theorem smul_add :
∀ {M : Type u_1} {A : Type u_4} [inst : AddZeroClass A] [inst_1 : DistribSMul M A] (a : M) (b₁ b₂ : A),
a • (b₁ + b₂) = a • b₁ + a • b₂
This theorem, `smul_add`, states that for any types `M` and `A`, given that `A` is an `AddZeroClass` and there exists a scalar multiplication (`DistribSMul`) operation from `M` to `A`, the scalar product of `a`, an instance of `M`, with the addition of `b₁` and `b₂`, instances of `A`, is equal to the sum of the scalar product of `a` with `b₁` and the scalar product of `a` with `b₂`. In mathematical notation, for any scalar `a` and vectors `b₁`, `b₂`, we have: `a • (b₁ + b₂) = a • b₁ + a • b₂`. This is one of the standard axioms for a vector space.
More concisely: For any type `M` with scalar multiplication `DistribSMul` over an additive zero class `A`, the scalar product of an element `a` from `M` with the sum of two elements `b₁` and `b₂` from `A` equals the sum of the scalar products of `a` with `b₁` and `b₂`.
|
VAdd.comp.isScalarTower
theorem VAdd.comp.isScalarTower :
∀ {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [inst : VAdd M α] [inst_1 : VAdd M β]
[inst_2 : VAdd α β] [inst_3 : VAddAssocClass M α β] (g : N → M), VAddAssocClass N α β
This theorem states that given a sequential additive action structure from `M` to `α` and from `α` to `β` (a tower of additive actions), if we apply the composition of scalar multiplication (`SMul.comp`) to both of `M`'s actions using a function `g : N → M`, we would obtain a new sequence of additive action structure from `N` to `α` and from `α` to `β` (a new tower of scalar actions). However, this cannot be used as an instance because it could cause infinite loops when the `SMul` arguments are undetermined.
More concisely: Given a sequential additive action structure from `M` to `α` and from `α` to `β`, the function `g : N → M` induces a new tower of additive actions from `N` to `α` and from `α` to `β` by applying `SMul.comp` to the actions of `M`. However, this cannot be used as an instance due to potential infinite loops in the `SMul` arguments.
|
VAdd.comp.vaddCommClass'
theorem VAdd.comp.vaddCommClass' :
∀ {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [inst : VAdd M α] [inst_1 : VAdd β α]
[inst_2 : VAddCommClass β M α] (g : N → M), VAddCommClass β N α
This theorem states that for any types `M`, `N`, `α`, and `β`, given the instances of `VAdd` operation for `M` and `α`, and for `β` and `α`, as well as an instance of `VAddCommClass` for `β`, `M`, and `α`, if we have a function `g` mapping `N` to `M`, then there exists an instance of `VAddCommClass` for `β`, `N`, and `α`. Here, `VAdd` refers to the operation of vector addition, and `VAddCommClass` is a class that asserts the commutativity of vector addition. This implies that the commutative property of vector addition holds even when the vectors are mapped through a function.
More concisely: Given types `M`, `N`, `α`, and `β`, and instances of `VAdd` for `M` and `α`, `β` and `α`, and `VAddCommClass` for `β`, `M`, and `α`, if we have a function `g` from `N` to `M`, then there exists a `VAddCommClass` instance for `β`, `N`, and `α`.
|
one_smul_eq_id
theorem one_smul_eq_id :
∀ (M : Type u_1) {α : Type u_6} [inst : Monoid M] [inst_1 : MulAction M α], (fun x => 1 • x) = id
This theorem, `one_smul_eq_id`, states that for any type `M` that is a monoid, and any type `α` on which `M` acts via multiplication, multiplying by the monoid's identity element (1) is the same as applying the identity function. In other words, for all elements `x` of type `α`, `1 • x` equals `x`.
More concisely: For any monoid `M` and type `α` on which `M` acts by multiplication, the identity element of `M` (1) maps every element `x` of `α` to itself (i.e., `1 • x = x`).
|
AddAction.zero_vadd
theorem AddAction.zero_vadd :
∀ {G : Type u_10} {P : Type u_11} [inst : AddMonoid G] [self : AddAction G P] (p : P), 0 +ᵥ p = p
This theorem, `AddAction.zero_vadd`, states that zero acts as a neutral element for the operation `+ᵥ` in the context of additive action. In other words, for any type `G` that is an additive monoid and any type `P` upon which `G` acts additively (denoted as `[AddAction G P]`), adding `0` from `G` to any element `p` from `P` using the `+ᵥ` operation yields `p` unchanged.
More concisely: For any additive monoid `G` and any type `P` with additive action `[AddAction G P]`, the operation `+ᵥ` with `G` as the additive monoid and any element `p` in `P` satisfies `p +ᵥ 0 = p`.
|
DistribMulAction.smul_zero
theorem DistribMulAction.smul_zero :
∀ {M : Type u_10} {A : Type u_11} [inst : Monoid M] [inst_1 : AddMonoid A] [self : DistribMulAction M A] (a : M),
a • 0 = 0
This theorem states that, for any type `M` that forms a monoid and any type `A` that forms an additive monoid, if `A` is a distributive multiplication action over `M`, then the result of scaling the zero element of `A` by any element of `M` is still the zero element of `A`. In other words, for any scalar `a` from `M`, `a` scaled by zero equals zero. This is a generalization of the familiar arithmetic rule that any number multiplied by zero equals zero.
More concisely: For any monoid `M` and additive monoid `A` with a distributive multiaction, multiplying any scalar `a` from `M` by the zero element of `A` results in the zero element of `A`.
|
SMul.comp.smulCommClass'
theorem SMul.comp.smulCommClass' :
∀ {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [inst : SMul M α] [inst_1 : SMul β α]
[inst_2 : SMulCommClass β M α] (g : N → M), SMulCommClass β N α
This theorem states that for any types `M`, `N`, `α`, and `β`, if `α` is a scalar multiplication space over `M` and `β`, and `β` and `M` commute for scalar multiplication on `α`, then for any function `g` from `N` to `M`, `β` and `N` also commute for scalar multiplication on `α`. However, this theorem cannot be an instance because it can cause infinite loops whenever the `SMul` arguments are still metavariables.
More concisely: For any types `M`, `N`, scalar multiplication space `α` over `M`, and commuting scalars `β` and `M`, if `g` is a function from `N` to `M`, then `β` and `N` commute for scalar multiplication on `α`.
|
comp_smul_left
theorem comp_smul_left :
∀ (M : Type u_1) {α : Type u_6} [inst : Monoid M] [inst_1 : MulAction M α] (a₁ a₂ : M),
((fun x => a₁ • x) ∘ fun x => a₂ • x) = fun x => (a₁ * a₂) • x
This theorem, `comp_smul_left`, states that for any type `M` with a Monoid structure and another type `α` with a Multiplicative Action by `M`, the composition of scalar multiplication functions `a₁ • _` and `a₂ • _` is equal to the function corresponding to scalar multiplication by `(a₁ * a₂)`. This is essentially saying that scalar multiplication in this context is associative.
More concisely: For types `M` with a Monoid structure and `α` with a multiplicative action by `M`, the scalar multiplication functions `(a₁ • _)` and `(a₂ • _)` commute, i.e., `(a₁ • a₂) • x = a₁ • (a₂ • x)` for all `x : α`.
|
Function.Injective.smulCommClass
theorem Function.Injective.smulCommClass :
∀ {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [inst : SMul M α] [inst_1 : SMul N α]
[inst_2 : SMul M β] [inst_3 : SMul N β] [inst_4 : SMulCommClass M N β] {f : α → β},
Function.Injective f →
(∀ (c : M) (x : α), f (c • x) = c • f x) → (∀ (c : N) (x : α), f (c • x) = c • f x) → SMulCommClass M N α
The theorem `Function.Injective.smulCommClass` states that for any types `M`, `N`, `α`, and `β`, if `α` and `β` have scalar multiplication structures by `M` and `N`, and if `β` has a scalar multiplication commutation structure between `M` and `N`, then for any function `f` from `α` to `β` that is injective and respects the scalar multiplication (i.e., `f` of `c` multiplied by `x` is equal to `c` multiplied by `f` of `x` for any scalar `c` and any element `x` of `α`), `α` also has a scalar multiplication commutation structure between `M` and `N`.
In simpler terms, if the function `f` is injective and preserves the scalar multiplication operation, then the property of commuting scalar multiplications is transferred from the codomain `β` to the domain `α` of the function.
More concisely: If `α` and `β` are types with scalar multiplication structures by `M` and `N`, `β` has a scalar multiplication commutation structure between `M` and `N`, and `f` : `α → β` is an injective homomorphism of additive monoids (respecting scalar multiplications), then `α` has a scalar multiplication commutation structure between `M` and `N`.
|
DistribMulAction.smul_add
theorem DistribMulAction.smul_add :
∀ {M : Type u_10} {A : Type u_11} [inst : Monoid M] [inst_1 : AddMonoid A] [self : DistribMulAction M A] (a : M)
(x y : A), a • (x + y) = a • x + a • y
This theorem states that scalar multiplication distributes over addition in a distributive multiplicative action context. Specifically, if you have elements `a` of type `M` (a monoid), and `x` and `y` of type `A` (an additive monoid), then the scalar multiplication of `a` with the sum of `x` and `y` is equivalent to the sum of the scalar multiplication of `a` with `x` and `a` with `y`. This is encapsulated in the familiar formula `a • (x + y) = a • x + a • y`.
More concisely: For any monoid element `a` and additive monoid elements `x` and `y`, scalar multiplication distributes over addition: `a • (x + y) = a • x + a • y`.
|
AddAction.exists_vadd_eq
theorem AddAction.exists_vadd_eq :
∀ (M : Type u_1) {α : Type u_6} [inst : VAdd M α] [inst_1 : AddAction.IsPretransitive M α] (x y : α),
∃ m, m +ᵥ x = y
This theorem states that for any type `M` and any type `α` where `α` has a vector addition operation with `M` and an associated pretransitive addition action, for any elements `x` and `y` of type `α`, there exists an element `m` of type `M` such that adding `m` to `x` using vector addition gives `y`. In mathematical terms, we could say: "Given any two elements in a space that supports vector addition, there exists a vector that can translate one element into the other."
More concisely: For any type `α` with vector addition and pretransitive action, and for any `x` and `y` in `α`, there exists an element `m` in `M` such that `x + m = y`.
|
MulAction.exists_smul_eq
theorem MulAction.exists_smul_eq :
∀ (M : Type u_1) {α : Type u_6} [inst : SMul M α] [inst_1 : MulAction.IsPretransitive M α] (x y : α),
∃ m, m • x = y
This theorem states that for any two elements `x` and `y` of a certain type `α`, in the context where `α` is a set on which a type `M` acts via scalar multiplication (`SMul`) and this action is pretransitive (`MulAction.IsPretransitive`), there exists an element `m` of type `M` such that the scalar multiplication of `m` and `x` equals `y`. In mathematical terms, given any `x` and `y` in `α`, there exists `m` in `M` such that `m * x = y`.
More concisely: For any `x` and `y` in a set `α` with respect to an pretransitive `M`-module structure on `α`, there exists an element `m` in `M` such that `m * x = y`.
|
vadd_assoc
theorem vadd_assoc :
∀ {α : Type u_6} {M : Type u_10} {N : Type u_11} [inst : VAdd M N] [inst_1 : VAdd N α] [inst_2 : VAdd M α]
[inst_3 : VAddAssocClass M N α] (x : M) (y : N) (z : α), x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)
This theorem, `vadd_assoc`, states that for any types `α`, `M`, `N` where `M` and `N` are vectorially added to get `α`, the operation of vector addition (denoted by `+ᵥ`) is associative. That is, given elements `x` of type `M`, `y` of type `N`, and `z` of type `α`, adding `y` and `z` together (with vector addition) first, then adding `x` to the result is the same as adding `x` and `y` together first (with vector addition), then adding `z` to the result. This theorem requires the assumption that the types `M`, `N`, and `α` form a `VAddAssocClass` which essentially means that vector addition between these types is associative.
More concisely: For types `M`, `N`, and `α` forming a `VAddAssocClass`, the vector addition operation `+ᵥ` is associative, i.e., `(x +ᵥ y) +ᵥ z = x +ᵥ (y +ᵥ z)` for all `x : M`, `y : N`, and `z : α`.
|
MulAction.mul_smul
theorem MulAction.mul_smul :
∀ {α : Type u_10} {β : Type u_11} [inst : Monoid α] [self : MulAction α β] (x y : α) (b : β),
(x * y) • b = x • y • b
This theorem, `MulAction.mul_smul`, states that for any two elements `x` and `y` of a monoid `α` and any element `b` of a set `β` on which `α` acts (i.e., `α` is a MulAction on `β`), the action of the product of `x` and `y` on `b` is the same as the action of `x` on the result of the action of `y` on `b`. In other words, the multiplication operation (`*`) on `α` and the scalar multiplication operation (`•`) on `β` are associative. In mathematical terms, we can write this as `(x * y) • b = x • (y • b)` for all `x`, `y` in `α` and `b` in `β`.
More concisely: For any monoid action `α` on a set `β` and elements `x`, `y` in `α` and `b` in `β`, we have `(x * y) • b = x • (y • b)`.
|
smul_pow
theorem smul_pow :
∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : MulAction M N]
[inst_3 : IsScalarTower M N N] [inst_4 : SMulCommClass M N N] (r : M) (x : N) (n : ℕ),
(r • x) ^ n = r ^ n • x ^ n
The theorem `smul_pow` states that for any two types `M` and `N` where `M` is a monoid, `N` is a monoid, there is a multiplication action of `M` on `N`, `N` is a scalar tower over `M`, and the scalar multiplication on `M` and `N` commutes, if you have an element `r` of `M`, an element `x` of `N`, and a natural number `n`, then the `n`-th power of the scalar multiplication of `r` and `x` is equal to the scalar multiplication of the `n`-th power of `r` and the `n`-th power of `x`. In mathematical terms, this can be written as `(r • x) ^ n = r ^ n • x ^ n`.
More concisely: For any monoids M and N with scalar multiplication action on N commuting with scalar multiplication, and any element r in M and natural number n, (r * x) ^ n = r ^ n * x ^ n holds for all x in N.
|
smul_mul_assoc
theorem smul_mul_assoc :
∀ {α : Type u_6} {β : Type u_7} [inst : Mul β] [inst_1 : SMul α β] [inst_2 : IsScalarTower α β β] (r : α) (x y : β),
r • x * y = r • (x * y)
This theorem, `smul_mul_assoc`, states that for any scalars `r` and any elements `x`, `y` of a multiplication structure `β` (over which `α` is a scalar multiplication), the operation of scalar multiplication `r • x` followed by multiplication with `y` (`r • x * y`) is the same as scalar multiplication of `r` with the product of `x` and `y` (`r • (x * y)`). This is an important property related to the associativity of multiplication and scalar multiplication in algebraic structures where `α` acts as a scalar on `β` (usually satisfied by `Algebra α β`).
More concisely: For any multiplication structure β and scalars r of α, the association holds between scalar multiplication and multiplication: r • (x * y) = r • x * y.
|
SMulCommClass.smul_comm
theorem SMulCommClass.smul_comm :
∀ {M : Type u_10} {N : Type u_11} {α : Type u_12} [inst : SMul M α] [inst_1 : SMul N α] [self : SMulCommClass M N α]
(m : M) (n : N) (a : α), m • n • a = n • m • a
This theorem states that the scalar multiplication operation '•' is left-commutative. Specifically, for any types M, N, and α (with α being a scalar multiple of M and N), and given the scalar multiplication commutativity class of M, N, and α, the order in which the elements of types M and N are scalar-multiplied with an element of type α does not affect the result. In mathematical terms, if m is an element of type M, n is an element of type N, and a is an element of type α, then m scalar-multiplied with (n scalar-multiplied with a) is equal to n scalar-multiplied with (m scalar-multiplied with a), i.e., `m • n • a = n • m • a`.
More concisely: For any types M, N, and scalar α, the left-commutativity of scalar multiplication holds: m • (n • α) = n • (m • α) for all m : M and n : N.
|
VAddCommClass.vadd_comm
theorem VAddCommClass.vadd_comm :
∀ {M : Type u_10} {N : Type u_11} {α : Type u_12} [inst : VAdd M α] [inst_1 : VAdd N α] [self : VAddCommClass M N α]
(m : M) (n : N) (a : α), m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a)
The theorem `VAddCommClass.vadd_comm` states that the vector addition operation `+ᵥ` is left commutative. Specifically, given any elements `m` of type `M`, `n` of type `N`, and `a` of type `α`, where `M` and `N` are types with vector addition structures (`VAdd M α` and `VAdd N α` respectively) and `α` is a type for which `M` and `N` are deemed to form a left-commutative vector addition class (`VAddCommClass M N α`), the result of adding `m` and `a` (after adding `n` to `a`) is the same as the result of adding `n` and `a` (after adding `m` to `a`). In mathematical notation, this is equivalent to saying that `m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a)`.
More concisely: For types `M` and `N` with left-commutative vector addition structures `VAdd M α` and `VAdd N α`, and for elements `m : M`, `n : N`, and `a : α`, we have `m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a)`.
|
smul_zero
theorem smul_zero : ∀ {M : Type u_1} {A : Type u_4} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0
This theorem states that for any type `M` and any type `A` where `A` has a zero element and `M` and `A` form a scalar multiplication zero class (which means `M` can be a scalar multiple of `A` and when scalar multiplied by zero gives zero), then the scalar multiplication of any element of `M` with the zero element of `A` is equal to zero. In mathematical notation, this can be represented as: for all `a` in `M`, `a * 0 = 0`.
More concisely: For any type `M` with scalar multiplication by a type `A` having a zero element, `a * 0 = 0` for all `a` in `M`.
|
VAddCommClass.symm
theorem VAddCommClass.symm :
∀ (M : Type u_10) (N : Type u_11) (α : Type u_12) [inst : VAdd M α] [inst_1 : VAdd N α]
[inst_2 : VAddCommClass M N α], VAddCommClass N M α
This theorem states that the commutativity of additive actions is a symmetric relation. Given three types `M`, `N`, and `α`, if `M` and `α` form an additive action and `N` and `α` form an additive action, and if there is a commutative relation between `M`, `N` and `α`, then the same commutative relation also exists between `N`, `M` and `α`. In simpler terms, if 'adding' elements of type `M` and `N` to an element of type `α` is commutative, then 'adding' elements of type `N` and `M` is also commutative. The theorem cannot be an instance because it would cause a loop in the instance search graph in Lean.
More concisely: If `M` and `α`, and `N` and `α` form commutative additive actions, then the commutativity of their addition with `α` implies the commutativity of `N` and `M` addition with `α`.
|
mul_smul_comm
theorem mul_smul_comm :
∀ {α : Type u_6} {β : Type u_7} [inst : Mul β] [inst_1 : SMul α β] [inst_2 : SMulCommClass α β β] (s : α) (x y : β),
x * s • y = s • (x * y)
This theorem, named `mul_smul_comm`, states that for all types `α` and `β`, where `β` has a multiplication operation, `α` can be scalar multiplied with `β`, and the scalar multiplication is commutative, then the multiplication of `β` and scalar multiplication of `α` and `β` are communicative. In mathematical terms, it asserts that for any scalar `s` and elements `x` and `y` of `β`, the equation `x * s • y = s • (x * y)` holds true. An algebra over `α` on `β` typically satisfies the scalar multiplication commutativity required in this theorem.
More concisely: For all types `α` and `β` with a commutative scalar multiplication, and for all scalars `s` and elements `x` and `y` of `β`, `x * s * y = s * (x * y)`.
|
IsCentralVAdd.op_vadd_eq_vadd
theorem IsCentralVAdd.op_vadd_eq_vadd :
∀ {M : Type u_10} {α : Type u_11} [inst : VAdd M α] [inst_1 : VAdd Mᵃᵒᵖ α] [self : IsCentralVAdd M α] (m : M)
(a : α), AddOpposite.op m +ᵥ a = m +ᵥ a
This theorem states that for any types `M` and `α`, where `M` and `αᵃᵒᵖ` both have vector addition structures (`VAdd`), and `M` is a central element with respect to the vector addition on `α` (`IsCentralVAdd M α`), the right and left actions of `M` on `α` are the same. In other words, for any element `m` of `M` and any element `a` of `α`, the operation of adding `m` (considered as an element of `Mᵃᵒᵖ` via `AddOpposite.op`) to `a` on the left is equal to the operation of adding `m` to `a` on the right.
More concisely: For any types `M` and `α` with vector addition structures where `M` is a central element with respect to `α`, the left and right actions of `M` on `α` via vector addition agree.
|
VAddAssocClass.vadd_assoc
theorem VAddAssocClass.vadd_assoc :
∀ {M : Type u_10} {N : Type u_11} {α : Type u_12} [inst : VAdd M N] [inst_1 : VAdd N α] [inst_2 : VAdd M α]
[self : VAddAssocClass M N α] (x : M) (y : N) (z : α), x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)
This theorem, `VAddAssocClass.vadd_assoc`, is about the associativity of the vector addition operation (`+ᵥ`). It states that for any types `M`, `N`, and `α` with defined vector addition operations, if these types form an associative class for vector addition, then for any elements `x` of type `M`, `y` of type `N`, and `z` of type `α`, the operation of adding `x` to `y`, and then the result to `z` is the same as adding `x` to the result of adding `y` to `z`. This is expressed in the form `x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)`. This theorem validates the general property of associativity for this specific operation in the mentioned context.
More concisely: For types `M`, `N`, and `α` with defined and associative vector addition operations, `x +ᵥ (y +ᵥ z) = x +ᵥ y +ᵥ z` for all `x` of type `M`, `y` of type `N`, and `z` of type `α`.
|
AddAction.IsPretransitive.exists_vadd_eq
theorem AddAction.IsPretransitive.exists_vadd_eq :
∀ {M : Type u_10} {α : Type u_11} [inst : VAdd M α] [self : AddAction.IsPretransitive M α] (x y : α),
∃ g, g +ᵥ x = y
This theorem states that for any two elements `x` and `y` of a certain type `α` that has a vector addition operation with a type `M`, given that `M` acts on `α` in a pretransitive manner (i.e., for any pair of elements in `α`, there is an element in `M` that, when vector-added to the first element, yields the second), there exists an element `g` in `M` such that the result of vector-adding `g` to `x` is `y`. In terms of vector spaces, this means that you can get from any vector `x` to any other vector `y` by adding a certain vector `g`.
More concisely: Given a type `α` with pretransitive vector addition `+` with type `M`, for any `x, y ∈ α`, there exists `g ∈ M` such that `x + g = y`.
|
smul_one_smul
theorem smul_one_smul :
∀ {α : Type u_6} {M : Type u_10} (N : Type u_11) [inst : Monoid N] [inst_1 : SMul M N] [inst_2 : MulAction N α]
[inst_3 : SMul M α] [inst_4 : IsScalarTower M N α] (x : M) (y : α), (x • 1) • y = x • y
This theorem states that for any types `α`, `M`, `N`, given an instance of `Monoid` over `N`, an instance of `SMul` over `M` and `N`, an instance of `MulAction` over `N` and `α`, an instance of `SMul` over `M` and `α`, and an instance of `IsScalarTower` over `M`, `N`, and `α`, for any elements `x` of type `M` and `y` of type `α`, scalar multiplication of `y` by `x • 1` is the same as scalar multiplication of `y` by `x`. In other words, the scalar multiplication of `y` by `x` is not affected by multiplying `x` by the multiplicative identity `1` in the `SMul` structure, which is consistent with the principle that multiplying by the identity element should not change the value.
More concisely: For any types `M` with a Monoid structure, `N`, `α`, given instances of `SMul` for `M` and `N`, `M` and `α`, `MulAction` for `N` and `α`, and `IsScalarTower` over `M`, `N`, and `α`, scalar multiplication of `α` by `x` is commutative with multiplication of `x` by the multiplicative identity `1` in `M`.
|
smul_mul_smul
theorem smul_mul_smul :
∀ {M : Type u_1} {α : Type u_6} [inst : Monoid M] [inst_1 : MulAction M α] [inst_2 : Mul α] (r s : M) (x y : α)
[inst_3 : IsScalarTower M α α] [inst_4 : SMulCommClass M α α], r • x * s • y = (r * s) • (x * y)
This theorem, `smul_mul_smul`, states that for any types `M` and `α`, where `M` is a monoid and `α` has both a multiplication action by `M` and a multiplication operation, and for any elements `r` and `s` in `M` and `x` and `y` in `α`, the scalar multiplication of `r` and `x` times the scalar multiplication of `s` and `y` equals the scalar multiplication of `r * s` and `x * y`. This holds when the scalar multiplication is compatible with the multiplication in `α` (i.e., `α` is a scalar tower over `M`) and the scalar multiplication by `M` commutes with the multiplication in `α`. Note that these conditions are usually satisfied when `M` is an algebra over `α`.
More concisely: For any monoid `M` acting on a type `α` with compatible scalar multiplications and commuting multiplications, the scalar multiplication of an element `r` in `M` with an element `x` in `α`, and the scalar multiplication of an element `s` in `M` with an element `y` in `α`, are equal to the scalar multiplication of their product `r * s` in `M` with the product of `x` and `y` in `α`.
|
MulAction.isPretransitive_compHom
theorem MulAction.isPretransitive_compHom :
∀ {E : Type u_10} {F : Type u_11} {G : Type u_12} [inst : Monoid E] [inst_1 : Monoid F] [inst_2 : MulAction F G]
[inst_3 : MulAction.IsPretransitive F G] {f : E →* F}, Function.Surjective ⇑f → MulAction.IsPretransitive E G
The theorem `MulAction.isPretransitive_compHom` states that for any types `E`, `F`, and `G`, if `E` and `F` are monoids and there is a multiplication action of `F` on `G` that is transitive, then the action of `E` on `G`, obtained by composing the action of `F` on `G` with a surjective homomorphism from `E` to `F`, is also transitive. In other words, transitivity of an action is preserved under surjective homomorphisms.
More concisely: If `F` is a transitive monoid action on `G` and there is a surjective homomorphism from monoid `E` to `F`, then `E` acts transitively on `G` through the action induced by the given homomorphism.
|
IsCentralScalar.op_smul_eq_smul
theorem IsCentralScalar.op_smul_eq_smul :
∀ {M : Type u_10} {α : Type u_11} [inst : SMul M α] [inst_1 : SMul Mᵐᵒᵖ α] [self : IsCentralScalar M α] (m : M)
(a : α), MulOpposite.op m • a = m • a
The theorem `IsCentralScalar.op_smul_eq_smul` states that, for any types `M` and `α` where `M` and the multiplicative opposite of `M`, denoted `Mᵐᵒᵖ`, can act on `α` by scalar multiplication (expressed by the type classes `SMul M α` and `SMul Mᵐᵒᵖ α`), and where `M` is a central scalar of `α` (expressed by the type class `IsCentralScalar M α`), the result of the right or left action of an element `m : M` on an element `a : α` is the same. In other words, the scalar multiplication of `a` by the multiplicative opposite of `m` is equal to the scalar multiplication of `a` by `m`. This is expressed in mathematical notation as $m^{op} \cdot a = m \cdot a$ for all `m : M` and `a : α`.
More concisely: For any type `M` and `α` with `IsCentralScalar M α`, and for all `m : M` and `a : α`, $m^{op} \cdot a = m \cdot a$.
|
SMul.comp.smulCommClass
theorem SMul.comp.smulCommClass :
∀ {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [inst : SMul M α] [inst_1 : SMul β α]
[inst_2 : SMulCommClass M β α] (g : N → M), SMulCommClass N β α
This theorem establishes that for any types `M`, `N`, `α`, and `β`, given that `M` and `β` are semimultiplicative over `α`, and that `M` and `β` commute over `α` (as expressed by `SMulCommClass M β α`), then for any function `g` from `N` to `M`, `N` and `β` will also commute over `α`. In other words, the commutative property between `M` and `β` over `α` is preserved when `M` is mapped to another type `N` through a function `g`. Note that this cannot be set as an instance automatically by Lean as it can cause infinite loops when the `SMul` arguments are still metavariables.
More concisely: If types `M`, `N`, `α`, and `β` are such that `M` and `β` are semimultiplicative and commute over `α`, then for any function `g` from `N` to `M`, `β` and the image of `β` under `g` commute over `α`.
|
smul_one_mul
theorem smul_one_mul :
∀ {M : Type u_10} {N : Type u_11} [inst : MulOneClass N] [inst_1 : SMul M N] [inst_2 : IsScalarTower M N N] (x : M)
(y : N), x • 1 * y = x • y
This theorem, `smul_one_mul`, states that for any types `M` and `N`, given a multiplication identity element (with `N` acting as a `MulOneClass`), a scalar multiplication operation (`SMul`) between `M` and `N`, and a scalar tower (`IsScalarTower`) that is a structure expressing the associativity between the scalar multiplication and the multiplication, then for any element `x` of type `M` and `y` of type `N`, the scalar multiple of `1` and `y` by `x` is equal to the scalar multiple of `y` by `x`. This essentially shows the neutral aspect of `1` in scalar multiplication context.
More concisely: For any types `M`, `N` with `N` being a `MulOneClass`, given a scalar multiplication `SMul` and a scalar tower `IsScalarTower` between `M` and `N`, the scalar multiplication of `1` by any `y` in `N` by an element `x` in `M` equals the scalar multiplication of `y` by `x`.
|
one_smul
theorem one_smul : ∀ (M : Type u_1) {α : Type u_6} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = b := by
sorry
This theorem, `one_smul`, states that for every type `M` and for a given type `α`, given that `M` is a monoid and there exists a multiplication action (`MulAction`) of `M` on `α`, the action of the identity element (`1` of the monoid) on any element `b` of type `α` is equal to the element `b` itself. In other words, multiplying any element by the identity in this context leaves it unchanged.
More concisely: For any monoid `M` and type `α` with a multiplication action, the identity element of `M` acts as the identity on elements of `α`, i.e., `1 * x = x` for all `x` in `α`.
|
SMul.comp.isScalarTower
theorem SMul.comp.isScalarTower :
∀ {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [inst : SMul M α] [inst_1 : SMul M β]
[inst_2 : SMul α β] [inst_3 : IsScalarTower M α β] (g : N → M), IsScalarTower N α β
This theorem states that for any types `M`, `N`, `α` and `β`, if we have scalar actions `M → α → β` forming a tower (meaning that the scalar multiplication is associative across the types), and there exists a map `g` from `N` to `M`, then we can construct a new tower of scalar actions `N → α → β` using `SMul.comp` to pull back `M`'s actions. However, this cannot be an instance as it can result in infinite loops when the `SMul` arguments are still not fully instantiated, i.e., when they are metavariables.
More concisely: Given types `M`, `N`, `α`, `β`, and a tower of scalar actions `M → α → β`, if there exists a map `g : N → M`, then we can construct a new tower of scalar actions `N → α → β` by pulling back `M`'s actions using `SMul.comp`. (However, this cannot be an instance due to potential infinite loops with uninstantiated `SMul` arguments.)
|
vadd_add_assoc
theorem vadd_add_assoc :
∀ {α : Type u_6} {β : Type u_7} [inst : Add β] [inst_1 : VAdd α β] [inst_2 : VAddAssocClass α β β] (r : α)
(x y : β), r +ᵥ x + y = r +ᵥ (x + y)
This theorem is asserting that for any types `α` and `β`, where `β` is an additive type and `α` and `β` are types that allow for vector addition, the operation of adding a scalar `r` to a vector `x`, and then adding a scalar `y`, is the same as adding `r` to the result of adding `x` and `y`. In mathematical terms, it's asserting that $r +ᵥ x + y = r +ᵥ (x + y)$ for all `r`, `x`, and `y` of appropriate types, where $+ᵥ$ denotes vector addition. This is essentially the associativity property in the context of vector addition.
More concisely: For any additive types `α` and scalar type `β`, the operation of adding a scalar `r` to the vector sum `x + y` is equivalent to adding the scalars `r` and `r` separately and then adding the vectors `x` and `y`, i.e., `r + (x + y) = r + x + y`.
|
comp_vadd_left
theorem comp_vadd_left :
∀ (M : Type u_1) {α : Type u_6} [inst : AddMonoid M] [inst_1 : AddAction M α] (a₁ a₂ : M),
((fun x => a₁ +ᵥ x) ∘ fun x => a₂ +ᵥ x) = fun x => a₁ + a₂ +ᵥ x
This theorem, `comp_vadd_left`, states that for any two elements, `a₁` and `a₂`, from an additively structured set `M`, and for any `x` in an additively acted upon set `α`, the composition of the vector addition functions with `a₁` and `a₂` respectively is the same as vector addition of `a₁ + a₂` with `x`. In math notation, this would mean `(a₁ +ᵥ (a₂ +ᵥ x)) = (a₁ + a₂) +ᵥ x`. This holds true for all `M` of a certain type with an AddMonoid structure and all `α` of a certain type with an AddAction of `M`.
More concisely: For any additively structured sets `M` and additively acted upon set `α`, and for all `a₁, a₂ ∈ M` and `x ∈ α`, the commutative property holds for the vector addition functions and element-wise addition, i.e., `(a₁ + a₂) +ᵥ x = a₁ +ᵥ (a₂ + x)`.
|
SMulCommClass.symm
theorem SMulCommClass.symm :
∀ (M : Type u_10) (N : Type u_11) (α : Type u_12) [inst : SMul M α] [inst_1 : SMul N α]
[inst_2 : SMulCommClass M N α], SMulCommClass N M α
This theorem states that the commutativity of actions, defined by the `SMulCommClass`, is a symmetric relation. This means that for any types `M`, `N`, and `α` where `M` and `N` are both types of actions on `α` and there exists a `SMulCommClass` instance for `M`, `N` and `α`, there will also exist a `SMulCommClass` instance for `N`, `M` and `α`. Note that this theorem cannot be an instance, as it would cause a loop in the instance search graph.
More concisely: For any types `M`, `N`, and `α` where `M` and `N` are actions on `α`, the `SMulCommClass` relation between `M` and `N` implies the `SMulCommClass` relation between `N` and `M`.
|
VAdd.comp.vaddCommClass
theorem VAdd.comp.vaddCommClass :
∀ {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [inst : VAdd M α] [inst_1 : VAdd β α]
[inst_2 : VAddCommClass M β α] (g : N → M), VAddCommClass N β α
This theorem states that for any types `M`, `N`, `α`, and `β`, given that `α` is a vector space over `M` and `β`, and the addition operation in the vector space `α` is commutative with respect to `M` and `β`, then for any function `g` from `N` to `M`, the addition operation in the vector space `α` is also commutative with respect to `N` and `β`. However, this theorem can't be an instance because it could cause infinite loops in the type class inference mechanism of Lean 4 when the arguments for the `VAdd` class are still metavariables.
More concisely: If `α` is a commutative vector space over `M` and `β`, then the addition operation in `α` is commutative with respect to `N` when viewed as a vector space over `M`, `β`, and `N`.
|
add_vadd_comm
theorem add_vadd_comm :
∀ {α : Type u_6} {β : Type u_7} [inst : Add β] [inst_1 : VAdd α β] [inst_2 : VAddCommClass α β β] (s : α) (x y : β),
x + (s +ᵥ y) = s +ᵥ (x + y)
This theorem states that for any types `α` and `β`, where `β` is an additive type and `α` and `β` form a vector addition structure that respects commutativity, the operation of adding a scalar `s` from `α` to a `β` value `y` and then adding that result to another `β` value `x` is the same as adding `x` and `y` first and then adding the scalar `s`. In mathematical notation, it asserts that for any `x`, `y` in `β` and `s` in `α`, we have `x + (s + y) = s + (x + y)`.
More concisely: For any additive types `β` and scalars `α`, the distributive property holds: `x + (s + y) = s + (x + y)` for all `x, y in β` and `s in α`.
|
AddAction.add_vadd
theorem AddAction.add_vadd :
∀ {G : Type u_10} {P : Type u_11} [inst : AddMonoid G] [self : AddAction G P] (g₁ g₂ : G) (p : P),
g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
This theorem, `AddAction.add_vadd`, states that for any two elements `g₁` and `g₂` of a type `G` with an additive monoid structure and any element `p` of a type `P` with an additive action by `G`, the action of `g₁ + g₂` on `p` (denoted `g₁ + g₂ +ᵥ p`) is equal to the result of first applying the action of `g₂` to `p` and then applying the action of `g₁` to the result (denoted `g₁ +ᵥ (g₂ +ᵥ p)`). In other words, the additive action `+ᵥ` is associative with respect to the addition `+` in `G`.
More concisely: For any additive monoid `G` with additive action `+ᵥ` by an additive monoid `P`, the action `g₁ +ᵥ (g₂ +ᵥ p)` equals `(g₁ + g₂) +ᵥ p` for all `g₁, g₂` in `G` and `p` in `P`.
|
smul_eq_mul
theorem smul_eq_mul : ∀ (α : Type u_10) [inst : Mul α] {a a' : α}, a • a' = a * a'
This theorem states that for any type `α` with a multiplication operation and for any two elements `a` and `a'` of type `α`, the scalar multiplication of `a` and `a'` is equal to the product of `a` and `a'`. In mathematical terms, we could write this as `a • a' = a * a'` for all `a` and `a'` in a type `α` with multiplication.
More concisely: For any type `α` equipped with a multiplication operation, the scalar multiplication equals the product operation: `a • a' = a * a'` for all `a, a' : α`.
|
zero_vadd_eq_id
theorem zero_vadd_eq_id :
∀ (M : Type u_1) {α : Type u_6} [inst : AddMonoid M] [inst_1 : AddAction M α], (fun x => 0 +ᵥ x) = id
This theorem, `zero_vadd_eq_id`, states that for any type `M` and any type `α` where `M` is an add monoid and there is an addition action of `M` on `α`, the function that adds the zero element of `M` to any element of `α` (denoted as `0 +ᵥ x`) is the same as the identity function. This means that adding zero does not change the value of any element in the set `α`.
More concisely: For any add monoid `M` and type `α` with an addition action, the operation `0 +ᵥ x` equals the identity function on `α`.
|
vadd_zero_add
theorem vadd_zero_add :
∀ {M : Type u_10} {N : Type u_11} [inst : AddZeroClass N] [inst_1 : VAdd M N] [inst_2 : VAddAssocClass M N N]
(x : M) (y : N), x +ᵥ 0 + y = x +ᵥ y
This theorem, `vadd_zero_add`, states that for any types `M` and `N`, where `N` has an instance of the `AddZeroClass` (meaning it has a zero element and addition operation), and there are vector addition operations (`VAdd`) defined on `M` and `N`, and the vector addition operation is associative (`VAddAssocClass`), then adding the zero element of `N` to the vector sum of an element `x` of `M` and another element `y` of `N` is equivalent to just adding `x` and `y`. In mathematical terms, it's saying that `x +ᵥ 0 + y = x +ᵥ y` for any `x` in `M` and `y` in `N`, where `+ᵥ` represents the vector addition operation.
More concisely: For types `M` and `N` with `AddZeroClass` instances, and associative vector addition `VAdd` on `M` and `N`, `x +ᵥ (y +ᵥ 0) = x +ᵥ y` for all `x` in `M` and `y` in `N`.
|
MulDistribMulAction.smul_mul
theorem MulDistribMulAction.smul_mul :
∀ {M : Type u_10} {A : Type u_11} [inst : Monoid M] [inst_1 : Monoid A] [self : MulDistribMulAction M A] (r : M)
(x y : A), r • (x * y) = r • x * r • y
The theorem `MulDistribMulAction.smul_mul` states that for any types `M` and `A` where `M` is a monoid and `A` is also a monoid, and `M` acts on `A` in a way that distributes over the multiplication operation in `A`, the operation of scalar multiplication by an element `r` of `M` is distributive over the multiplication of elements `x` and `y` in `A`. In other words, multiplying `r` with the product of `x` and `y` equals to the product of `r` multiplied with `x` and `r` multiplied with `y`.
More concisely: For any monoids M and A, and action of M on A satisfying left distribution property, for all r in M and x, y in A, we have r * (x * y) = (r * x) * y.
|
smul_smul
theorem smul_smul :
∀ {M : Type u_1} {α : Type u_6} [inst : Monoid M] [inst_1 : MulAction M α] (a₁ a₂ : M) (b : α),
a₁ • a₂ • b = (a₁ * a₂) • b
This theorem states that for any monoid `M` and any type `α` that has a multiplication action of `M` on it, the double scalar multiplication of two elements `(a₁, a₂)` from `M` and an element `b` from `α` is equal to the scalar multiplication of the product of `(a₁ * a₂)` and `b`. In other words, the scalar multiplication operation is associative with respect to the multiplication in the monoid. It means that scaling `b` by `a₁` and then by `a₂` is the same as scaling `b` by the product of `a₁` and `a₂`. This is expressed in mathematical notation as `a₁ • a₂ • b = (a₁ * a₂) • b`.
More concisely: For any monoid action of `M` on a type `α` and any `a₁, a₂ ∈ M` and `b ∈ α`, we have `a₁ * a₂ * b = (a₁ * a₂) * b`.
|
SMulZeroClass.smul_zero
theorem SMulZeroClass.smul_zero :
∀ {M : Type u_10} {A : Type u_11} [inst : Zero A] [self : SMulZeroClass M A] (a : M), a • 0 = 0
The theorem `SMulZeroClass.smul_zero` states that for any type `M` (representing scalars) and any type `A` (which has a zero element) that satisfies the `SMulZeroClass` property, multiplying zero from `A` by any scalar `a` from `M` results in zero. This is a foundational property in many areas of mathematics, such as in vector spaces, where any vector multiplied by zero scalar yields the zero vector.
More concisely: For any type `A` with a zero element and any type `M` of scalars satisfying `SMulZeroClass`, `a * 0 = 0` for all `a` in `M`.
|
MulAction.IsPretransitive.exists_smul_eq
theorem MulAction.IsPretransitive.exists_smul_eq :
∀ {M : Type u_10} {α : Type u_11} [inst : SMul M α] [self : MulAction.IsPretransitive M α] (x y : α),
∃ g, g • x = y
This theorem states that for any two elements `x` and `y` of a type `α` that has a multiplication action defined on it by a type `M`, there exists an element `g` of type `M` such that the multiplication action of `g` on `x` yields `y`. In other words, for any `x` and `y`, you can find a `g` such that when you "scale" `x` by `g`, you get `y`. This property is part of what it means for the multiplication action to be "pretransitive."
More concisely: For any type `α` with a multiplication action `M`, and for any `x, y ∈ α`, there exists `g ∈ M` such that `x * g = y`.
|
smul_sub
theorem smul_sub :
∀ {M : Type u_1} {A : Type u_4} [inst : Monoid M] [inst_1 : AddGroup A] [inst_2 : DistribMulAction M A] (r : M)
(x y : A), r • (x - y) = r • x - r • y
This theorem, `smul_sub`, states that for any types `M` and `A`, where `M` is a monoid, `A` is an add group, and there exists a distributive multiplication action of `M` on `A`, for any element `r` of `M` and any elements `x` and `y` of `A`, the scalar multiplication of `r` with the difference of `x` and `y` is equal to the difference of the scalar multiplication of `r` with `x` and the scalar multiplication of `r` with `y`. In mathematical terms, we can say $r * (x - y) = r * x - r * y$.
More concisely: For any monoid `M`, add group `A`, and distributive `M`-action on `A`, for all `r` in `M` and `x`, `y` in `A`, we have `r * (x - y) = r * x - r * y`.
|
smul_mul'
theorem smul_mul' :
∀ {M : Type u_1} {A : Type u_4} [inst : Monoid M] [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A] (a : M)
(b₁ b₂ : A), a • (b₁ * b₂) = a • b₁ * a • b₂
This theorem, `smul_mul'`, states that for any two types, `M` and `A`, where `M` is a monoid and `A` is also a monoid with an additional structure of a multiplication-distribution action of `M` on `A`, the scalar multiplication of a number `a` (from `M`) and the multiplication of any two elements `b₁` and `b₂` (from `A`), is equal to the multiplication of the scalar multiplication of `a` with `b₁` and the scalar multiplication of `a` with `b₂`. This is an important property that shows the compatibility of the scalar multiplication with the monoid multiplication in `A`.
More concisely: For any monoid `M` and monoid `A` with a multiplication-distribution action of `M` on `A`, the scalar multiplication of an element `a` in `M` with the product of elements `b₁` and `b₂` in `A` is equal to the product of the scalar multiplication of `a` with `b₁` and the scalar multiplication of `a` with `b₂`.
|
vadd_eq_add
theorem vadd_eq_add : ∀ (α : Type u_10) [inst : Add α] {a a' : α}, a +ᵥ a' = a + a'
This theorem, `vadd_eq_add`, states that for any type `α` that has an addition operation, the 'vector addition' of two elements `a` and `a'` of that type is equivalent to their standard addition. In other words, if you have two elements of a type that can be added together, the result of the 'vector addition' operation (represented by `+ᵥ`) is the same as the result of the standard addition operation (`+`).
More concisely: For any type `α` with addition `+`, the vector addition of two elements `a` and `a'` is equivalent to their standard addition: `a +ᵥ a' = a + a'`.
|