inv_smul_eq_iff₀
theorem inv_smul_eq_iff₀ :
∀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
a ≠ 0 → ∀ {x y : β}, a⁻¹ • x = y ↔ x = a • y
This theorem states that for any given types `α` and `β`, where `α` is a group with a multiplicative identity and a multiplicative inverse and zero, and `β` is a set where multiplication by an element of `α` is defined, for every non-zero `a` of type `α` and for all `x` and `y` of type `β`, `a⁻¹` (the multiplicative inverse of `a`) scaled by `x` equals `y` if and only if `x` equals `a` scaled by `y`.
More concisely: For any group `α` with identity and inverses, and any set `β` with defined multiplication by elements of `α`, the multiplicative inverses `a^{-1}` and `x` are equal if and only if `x` is equal to `a` scaled by `y` for some `y` in `β`.
|
smul_inv_smul
theorem smul_inv_smul :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : MulAction α β] (c : α) (x : β), c • c⁻¹ • x = x
This theorem states that for any group `α`, any type `β` that is a `MulAction` of `α`, any element `c` from the group `α`, and any element `x` from `β`, the following holds: if we perform the group operation (represented by `•`) on `c` and the inverse of `c` (represented by `c⁻¹`), and then perform the `MulAction` operation on the result and `x`, we get back `x`. In other words, `c • c⁻¹ • x = x`. This is essentially expressing that the multiplication action of an element and its inverse acts as the identity on `x`.
More concisely: For any group `α`, any `MulAction` `β` of `α`, and any `x` in `β` and `c` in `α`, we have `c • c⁻¹ • x = x`.
|
smul_left_cancel_iff
theorem smul_left_cancel_iff :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : MulAction α β] (g : α) {x y : β}, g • x = g • y ↔ x = y := by
sorry
This theorem, `smul_left_cancel_iff`, holds for a group `α` and a type `β` with a multiplication action `MulAction α β`. It states that for any element `g` of the group `α`, and any two elements `x` and `y` of type `β`, the statement "the result of the scalar multiplication of `g` and `x` is equal to the scalar multiplication of `g` and `y`" is equivalent to the statement "element `x` is equal to element `y`". In other words, if the same group element `g` acts on two objects `x` and `y` of type `β` yielding equal results, then `x` and `y` must be equal.
More concisely: For any group action of a group `α` on a type `β` with multiplication action `MulAction α β`, the scalar multiplication `g * x = g * y` implies `x = y`.
|
vadd_neg_vadd
theorem vadd_neg_vadd :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddAction α β] (c : α) (x : β), c +ᵥ (-c +ᵥ x) = x := by
sorry
This theorem states that for any type `α` that is an additive group, and any other type `β` that is an additive action of `α`, for any `c` of type `α` and `x` of type `β`, the vector addition of `c` and the vector addition of `-c` and `x` equals `x`. In mathematical notation, this can be written as: for all $c \in \alpha$ and $x \in \beta$, we have $c + (-c + x) = x$. This theorem essentially describes the cancellation property in the context of vector spaces.
More concisely: For any additive group `α` and additive action `β` of `α` on a type `β`, for all `c` in `α` and `x` in `β`, we have `c + (-c + x) = x`.
|
IsUnit.smul_left_cancel
theorem IsUnit.smul_left_cancel :
∀ {α : Type u} {β : Type v} [inst : Monoid α] [inst_1 : MulAction α β] {a : α},
IsUnit a → ∀ {x y : β}, a • x = a • y ↔ x = y
The theorem `IsUnit.smul_left_cancel` states that for any types `α` and `β`, where `α` is a monoid and `β` is a mulAction of `α`, for any element `a` of `α` that is a unit, and for any elements `x` and `y` of `β`, the statement `a • x = a • y` is equivalent to `x = y`. In other words, if `a` is a unit in the monoid `α`, then scalar multiplication by `a` is a cancelable operation on the left side, meaning that if `a` is multiplied with two elements `x` and `y` from `β` and the results are equal, then the original elements `x` and `y` must also be equal.
More concisely: If `α` is a monoid and `β` is a monoid action on `α`, for any unit `a` in `α` and any `x, y` in `β`, `a • x = a • y` implies `x = y`.
|
neg_vadd_vadd
theorem neg_vadd_vadd :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddAction α β] (c : α) (x : β), -c +ᵥ (c +ᵥ x) = x := by
sorry
This theorem, `neg_vadd_vadd`, states that for any types `α` and `β` where `α` is an additive group and there exists an additive action of `α` on `β`, for any elements `c` of type `α` and `x` of type `β`, the negative of `c` added with the vector sum of `c` and `x` is equal to `x`. In essence, it's showing an identity in the context of an additive group and its action on another type, similar to how in basic algebra, adding a number to its negation yields the identity element (0 for addition).
More concisely: For any additive group `α` acting on a type `β`, and for any elements `c` in `α` and `x` in `β`, we have `-c + x + c = x`.
|
AddAction.bijective
theorem AddAction.bijective :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddAction α β] (g : α),
Function.Bijective fun x => g +ᵥ x
The theorem `AddAction.bijective` asserts that for any type `α` equipped with an additive group structure, and any type `β` equipped with an add action of `α`, and any element `g` from `α`, the function that adds `g` to any element of `β` (`fun x => g +ᵥ x`) is bijective. In other words, for any group and action, translating by a group element gives a bijection from the set to itself.
More concisely: For any additive group `α` and any set `β` equipped with an additive action of `α`, the translation-by-element function `x ↦ g + x` is a bijection, where `g` is any element from `α`.
|
smul_inv_smul₀
theorem smul_inv_smul₀ :
∀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst_1 : MulAction α β] {c : α},
c ≠ 0 → ∀ (x : β), c • c⁻¹ • x = x
This theorem states that for any types `α` and `β`, given that `α` is a group with zero and `β` has a multiplication action by `α`, if `c` is a non-zero element of `α` and `x` is any element of `β`, then the result of scaling `x` by `c⁻¹` (the inverse of `c`) and then by `c` is equal to `x`. In mathematical terms, for any non-zero scalar `c` and any element `x`, we have `c * (c⁻¹ * x) = x`. This essentially confirms the cancellation property in a multiplicative group with zero.
More concisely: For any non-zero scalar `c` in a group with zero `α` and any element `x` in a type `β` with a right `α`-action, `c * (c⁻¹ * x) = x`.
|
MulAction.injective₀
theorem MulAction.injective₀ :
∀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
a ≠ 0 → Function.Injective fun x => a • x
The theorem `MulAction.injective₀` states that for all types `α` and `β`, where `α` is a group with zero and `β` is a set on which `α` acts multiplicatively, for any element `a` of `α` that is not zero, the function that maps any element `x` of `β` to the product of `a` and `x` (denoted as `a • x`) is injective. In other words, if `a • x = a • y` then `x` must be equal to `y`. This is applicable for any non-zero element `a` of the group `α`.
More concisely: For any non-zero element `a` in a group `α` and any sets `β` on which `α` acts multiplicatively, the function `x mapsto a • x` from `β` to itself is injective.
|
inv_smul_smul₀
theorem inv_smul_smul₀ :
∀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst_1 : MulAction α β] {c : α},
c ≠ 0 → ∀ (x : β), c⁻¹ • c • x = x
This theorem states that for any types `α` and `β`, where `α` is a group with zero and `β` is an object upon which `α` can act (denoted by `MulAction α β`), for any non-zero element `c` of `α` and any element `x` of `β`, if we first scale `x` by `c` and then scale the result by the multiplicative inverse of `c` (`c⁻¹`), we get `x` back. In mathematical terms, this theorem proves that the inverse scaling factor undoes the scaling, as long as the scaling factor is non-zero.
More concisely: For any group `α` with zero, any type `β` with `MulAction α β`, and any non-zero `c` in `α` and `x` in `β`, scaling `x` by `c` and then by `c⁻¹` yields `x`. In Lean notation, `(x : β) → c * x = x → c⁻¹ * (c * x) = x`.
|
smul_eq_zero_iff_eq
theorem smul_eq_zero_iff_eq :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : AddMonoid β] [inst_2 : DistribMulAction α β] (a : α) {x : β},
a • x = 0 ↔ x = 0
This theorem states that for any group `α`, add monoid `β`, and a distributive multiplication action of `α` on `β`, for any element `a` of `α` and any element `x` of `β`, the scalar multiplication of `a` and `x` equals zero if and only if `x` equals zero. Here, the scalar multiplication of `a` and `x` is represented as `a • x`. In other words, the only way for a scalar multiplication to yield zero in this context is when the element `x` from the add monoid is zero.
More concisely: For any group action by add monoid multiplication on an add monoid, the scalar multiplication of an element by another equals zero if and only if the second element is the additive identity.
|
MulAction.bijective
theorem MulAction.bijective :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : MulAction α β] (g : α), Function.Bijective fun x => g • x
The theorem `MulAction.bijective` states that for any type `α` of a group and any type `β` on which the group acts (represented by `MulAction α β`), for any element `g` of the group, the function that maps each element `x` in `β` to the product `g • x` is bijective. In other words, the action of multiplying by a fixed group element is a bijective function from `β` to itself. This means that it is both injective (no two different elements map to the same result) and surjective (every possible result is achieved by mapping some element).
More concisely: For any group `α` and any type `β` with a group action `MulAction α β`, the function `x mapsto g • x` is a bijective function on `β` for all `g` in `α`.
|
MulAction.injective
theorem MulAction.injective :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : MulAction α β] (g : α), Function.Injective fun x => g • x
The theorem `MulAction.injective` states that for every group `α` and every type `β` that is the target of a multiplication action of `α`, every element `g` of `α` defines an injective function. This injective function is defined as the multiplication of `g` with an element `x` from `β`. In other words, for any two elements `x` and `y` from `β`, if `g • x = g • y`, then it must be the case that `x = y`.
More concisely: Given a group `α` and a type `β` equipped with a multiplication action of `α`, the multiplication by each element `g` in `α` is an injective function on `β`.
|
AddAction.toPerm_injective
theorem AddAction.toPerm_injective :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddAction α β] [inst_2 : FaithfulVAdd α β],
Function.Injective AddAction.toPerm
The theorem `AddAction.toPerm_injective` states that for any additive group `α` and any type `β` upon which `α` acts additively, if this action is faithful (meaning that different elements of `α` act differently), then the function `AddAction.toPerm`, which maps each group element to the corresponding permutation of `β`, is injective. In other words, if for two elements `a` and `b` of the group `α`, the corresponding permutations of `β` are identical, then `a` must equal `b`.
More concisely: If `α` is an additive group acting faithfully on a type `β`, then the group homomorphism `AddAction.toPerm` from `α` to the permutaions of `β` is injective.
|
inv_smul_smul
theorem inv_smul_smul :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : MulAction α β] (c : α) (x : β), c⁻¹ • c • x = x
This theorem states that for every group `α` and every multiplicative action `MulAction α β` of `α` on `β`, for any element `c` in `α` and `x` in `β`, the inverse of `c` scaled by `c` scaled by `x` is equal to `x`. In mathematical terms, it says that if you have a group operation and a scalar multiplication operation (`•`), then scaling by `c` followed by scaling by the inverse of `c` (`c⁻¹`) is the same as doing nothing, i.e., it leaves `x` unchanged. This can be expressed as `c⁻¹ • c • x = x`.
More concisely: For every group action `MulAction α β` over a group `α`, and for all `c` in `α` and `x` in `β`, the association law holds: `c⁻¹ • c • x = x`.
|
AddAction.injective
theorem AddAction.injective :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddAction α β] (g : α),
Function.Injective fun x => g +ᵥ x
The theorem `AddAction.injective` states that for all types `α` and `β`, where `α` is an additive group and `β` is a set on which `α` acts additively, given any element `g` of type `α`, the function that adds `g` to an element `x` in `β` is injective. In other words, if `g +ᵥ x₁ = g +ᵥ x₂` then `x₁ = x₂`. This theorem ensures that additive actions preserve distinctness: different elements of the set will not be mapped to the same element by the additive action.
More concisely: For any additive group α and set β on which α acts additively, the function that maps x in β to g + x is injective for all g in α.
|
smul_eq_iff_eq_inv_smul
theorem smul_eq_iff_eq_inv_smul :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : MulAction α β] (g : α) {x y : β}, g • x = y ↔ x = g⁻¹ • y
This theorem states that for any group `α` and any set `β` with a multiplication action of `α` on `β`, and for any elements `g` in `α` and `x` and `y` in `β`, the statement that `g` multiplied by `x` equals `y` is equivalent to the statement that `x` equals the inverse of `g` multiplied by `y`. Here, `•` denotes the multiplication action of `α` on `β`, and `g⁻¹` denotes the inverse of `g` in the group `α`.
More concisely: For any group action of `α` on a set `β` and any `g` in `α` and `x, y` in `β`, `g • x = y` is equivalent to `x = g⁻¹ • y`.
|
MulAction.toPerm_injective
theorem MulAction.toPerm_injective :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : MulAction α β] [inst_2 : FaithfulSMul α β],
Function.Injective MulAction.toPerm
The theorem `MulAction.toPerm_injective` states that for any group `α` acting on a type `β` in a faithful manner (that is, distinct elements of `α` act differently on `β`), the function `MulAction.toPerm` is injective. In other words, if `MulAction.toPerm a = MulAction.toPerm b` for some elements `a` and `b` of the group `α`, then `a = b`. The function `MulAction.toPerm` converts a group element into a permutation of `β` induced by the group action, and the theorem asserts that distinct group elements give rise to distinct permutations when the action is faithful.
More concisely: In a faithful group action on a type, the induced permutation map is injective.
|
inv_smul_eq_iff
theorem inv_smul_eq_iff :
∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : MulAction α β] {a : α} {x y : β}, a⁻¹ • x = y ↔ x = a • y
This theorem states that for all types `α` and `β`, given `α` as a group and `β` as a set on which `α` acts multiplicatively (`MulAction α β`), for any elements `a` of `α` and `x`, `y` of `β`, the inverse of `a` (denoted `a⁻¹`) multiplied with `x` equals `y` if and only if `x` equals `a` multiplied with `y`. In mathematical notation, this is saying that for all `a` in `α` and `x`, `y` in `β`, `a⁻¹ * x = y` if and only if `x = a * y`.
More concisely: For all groups `α` and sets `β` with a multiplicative action of `α` on `β`, and for all `a` in `α` and `x`, `y` in `β`, `a⁻¹ * x = y` if and only if `x = a * y`.
|
vadd_left_cancel_iff
theorem vadd_left_cancel_iff :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddAction α β] (g : α) {x y : β},
g +ᵥ x = g +ᵥ y ↔ x = y
This theorem, `vadd_left_cancel_iff`, states that for any type `α` which is an AddGroup and any type `β` that is acted upon by `α` through addition, given an element `g` from `α` and two elements `x` and `y` from `β`, if the result of adding `g` to `x` is equal to the result of adding `g` to `y`, then `x` must be equal to `y`. In other words, this theorem provides the condition of left-cancellability in the context of additive actions.
More concisely: For any AddGroup `α` and any type `β` with an additive action, if for all `g` in `α` and `x, y` in `β`, `g + x = g + y` implies `x = y`, then `α` acts on `β` with left-cancellation.
|
neg_vadd_eq_iff
theorem neg_vadd_eq_iff :
∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddAction α β] {a : α} {x y : β},
-a +ᵥ x = y ↔ x = a +ᵥ y
This theorem states that for any types 'α' and 'β', where 'α' is an additive group and 'β' is an additive action of 'α', for any element 'a' of type 'α' and any elements 'x' and 'y' of type 'β', the equation "-a +ᵥ x = y" is equivalent to "x = a +ᵥ y". In other words, the operation of adding the negation of 'a' to 'x' in the vector space is the same as the operation of adding 'a' to 'y' in the vector space.
More concisely: For any additive group 'α' and additive action 'β' of 'α', for all elements 'a' in 'α' and 'x' and 'y' in 'β', the equations "-a ∘ x = y" and "x = a ∘ y" hold if and only if 'β' is an abelian group. (Here, '∘' denotes the additive action of 'α' on 'β' and the '-' sign denotes the additive inverse in 'α').
|