MulOpposite.op_surjective
theorem MulOpposite.op_surjective : ∀ {α : Type u_1}, Function.Surjective MulOpposite.op
The theorem `MulOpposite.op_surjective` states that for any type `α`, the function `MulOpposite.op` is surjective. This means that for every element of the opposite multiplicative group of `α` (denoted `αᵐᵒᵖ`), there is an element in `α` such that when the `MulOpposite.op` function is applied to it, we obtain the former element from the opposite multiplicative group. In other words, every element of the opposite multiplicative group can be reached by applying the `MulOpposite.op` function to some element of `α`.
More concisely: For every element in the opposite multiplicative group of type `α`, there exists an element in `α` that maps to it under the `MulOppositive.op` function.
|
MulOpposite.op_inv
theorem MulOpposite.op_inv : ∀ {α : Type u_1} [inst : Inv α] (x : α), MulOpposite.op x⁻¹ = (MulOpposite.op x)⁻¹ := by
sorry
The theorem `MulOpposite.op_inv` states that for any type `α` that has an inverse operation (specified by the `Inv α` instance), the multiplicative opposite of the inverse of an element `x` (denoted as `MulOpposite.op x⁻¹`) is equal to the inverse of the multiplicative opposite of `x` (denoted as `(MulOpposite.op x)⁻¹`). In other words, taking the multiplicative opposite and taking the inverse commute with each other.
More concisely: For any type `α` with an inverse operation, the multiplicative inverse of the multiplicative opposite of an element is equal to the multiplicative opposite of the inverse of that element. In other words, `(MulOpposite.op (Inv.inv x)) = Inv.inv (MulOpposite.op x)` for all `x : α`.
|
Mathlib.Algebra.Opposites._auxLemma.1
theorem Mathlib.Algebra.Opposites._auxLemma.1 :
∀ {α : Type u_1} {x y : α}, (MulOpposite.op x = MulOpposite.op y) = (x = y)
This theorem, named `_auxLemma.1` under the `Mathlib.Algebra.Opposites` namespace, states that for any type `α`, and any two elements `x` and `y` from this type, the operation `MulOpposite.op` applied to `x` being equal to the same operation applied to `y` is equivalent to `x` being equal to `y`. In other words, if the `MulOpposite.op` operation produces the same result for `x` and `y`, then `x` and `y` must be the same. This theorem plays a role in the manipulation of algebraic structures and their opposites in Lean 4, ensuring the integrity of operations on these structures.
More concisely: For any type `α` and elements `x` and `y` from `α`, `MulOpposite.op x = MulOpposite.op y` implies `x = y`.
|
MulOpposite.op_smul
theorem MulOpposite.op_smul :
∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] (a : α) (b : β), MulOpposite.op (a • b) = a • MulOpposite.op b
This theorem, `MulOpposite.op_smul`, states that for any type `α` and any type `R`, and given an instance of the scalar multiplication `SMul R α` between `R` and `α`, for any elements `c` of type `R` and `a` of type `α`, the operation `MulOpposite.op` applied to the scalar multiplication of `c` and `a` (i.e., `c • a`) is equal to the scalar multiplication of `c` and the `MulOpposite.op` of `a`. In other words, the `MulOpposite.op` operation distributes over scalar multiplication, a property often seen in algebraic structures.
More concisely: For any type `α` and scalar multiplication `SMul R α` over `R` on `α`, the scalar multiplication of an element `c` in `R` with the opposite `MulOpposite.op a` of an element `a` in `α` is equal to the scalar multiplication of `c` with `a`, i.e., `c • a = c • MulOpposite.op a`.
|
MulOpposite.op_mul
theorem MulOpposite.op_mul :
∀ {α : Type u_1} [inst : Mul α] (x y : α), MulOpposite.op (x * y) = MulOpposite.op y * MulOpposite.op x
This theorem states that for all elements `x` and `y` of a type `α` that has a multiplication operation, the "opposite multiplication" of the product of `x` and `y` (i.e., `MulOpposite.op (x * y)`) is equal to the product of the "opposite multiplication" of `y` and `x` (i.e., `MulOpposite.op y * MulOpposite.op x`). In other words, the operation `MulOpposite.op` reverses the order of multiplication, reflecting the property of the "opposite" or "reversed" multiplication.
More concisely: For all types `α` with a multiplication operation and for all elements `x` and `y` of `α`, the opposite multiplication of `x * y` is equal to `MulOpposite.op y * MulOpposite.op x`. In other words, `MulOpposite.op (x * y) = MulOpposite.op y * MulOpposite.op x`.
|
AddOpposite.op_surjective
theorem AddOpposite.op_surjective : ∀ {α : Type u_1}, Function.Surjective AddOpposite.op
The theorem `AddOpposite.op_surjective` states that for any type `α`, the function `AddOpposite.op` is surjective. In other words, for any element in the additive opposite type `αᵃᵒᵖ`, there exists at least one element in `α` such that, when the `AddOpposite.op` function is applied to it, the result is the given element in `αᵃᵒᵖ`.
More concisely: For every element in the additive opposite type of a type α, there exists an element in α mapping to it under the AddOpposite.op function.
|
MulOpposite.unop_injective
theorem MulOpposite.unop_injective : ∀ {α : Type u_1}, Function.Injective MulOpposite.unop
The theorem `MulOpposite.unop_injective` states that for any type `α`, the function `MulOpposite.unop` is injective. In other words, the function which takes an element from the opposite multiplication type `αᵐᵒᵖ` and returns its underlying element in `α` will always map distinct elements to distinct elements. If two elements in `αᵐᵒᵖ` have the same image in `α` under the `MulOpposite.unop` function, those two elements must have been the same to begin with.
More concisely: The function `MulOpposite.unop` from `αᵐᵒᵖ` to `α` is an injection.
|
MulOpposite.op_injective
theorem MulOpposite.op_injective : ∀ {α : Type u_1}, Function.Injective MulOpposite.op
The theorem `MulOpposite.op_injective` postulates that for all types `α`, the function `MulOpposite.op` is injective. This means that if two elements of type `α` are mapped to the same element in the multiplication-opposite type (denoted as `αᵐᵒᵖ`), then these two elements were originally equal. In other words, no two distinct elements of `α` are mapped to the same element of `αᵐᵒᵖ` by the `MulOpposite.op` function.
More concisely: The `MulOpposite.op` function maps distinct elements of type `α` to distinct elements in the multiplication-opposite type `αᵐᵒᵖ`.
|
MulOpposite.unop_surjective
theorem MulOpposite.unop_surjective : ∀ {α : Type u_1}, Function.Surjective MulOpposite.unop
The theorem `MulOpposite.unop_surjective` states that for any given type `α`, the function `MulOpposite.unop` is surjective. In other words, every element of the type `α` can be obtained by applying the `MulOpposite.unop` function to some element of the type `αᵐᵒᵖ`. Here, `αᵐᵒᵖ` represents the multiplicative opposite of `α` and `MulOpposite.unop` is a function that retrieves the original element from its multiplicative opposite.
More concisely: For any type `α`, the function `MulOpposite.unop` from the multiplicative opposite `αᵐᵒᵖ` to `α` is surjective.
|
Mathlib.Algebra.Opposites._auxLemma.6
theorem Mathlib.Algebra.Opposites._auxLemma.6 :
∀ {α : Type u_1} [inst : Zero α] (a : α), (MulOpposite.op a = 0) = (a = 0)
This theorem states that for any type `α` which has a zero element, and any element `a` of `α`, the `MulOpposite.op` operation of `a` is equal to zero if and only if `a` itself is equal to zero. In other words, the operation `MulOpposite.op` preserves the zero element in the type `α`.
More concisely: For any type `α` with a zero element and operation `MulOpposite.op`, `MulOpposite.op a = 0` if and only if `a = 0`.
|
AddOpposite.unop_surjective
theorem AddOpposite.unop_surjective : ∀ {α : Type u_1}, Function.Surjective AddOpposite.unop
The theorem `AddOpposite.unop_surjective` states that for any type `α`, the function `AddOpposite.unop` is surjective. In other words, for every element `b` of type `α`, there exists an element `a` of type `αᵃᵒᵖ` such that applying the function `AddOpposite.unop` to `a` results in `b`. This means that every element of type `α` can be obtained by applying `AddOpposite.unop` to some element of its additive opposite type `αᵃᵒᵖ`.
More concisely: For any type `α`, the function `AddOpposite.unop` from its additive opposite type `αᵃᵒᵖ` to `α` is surjective.
|
AddOpposite.op_injective
theorem AddOpposite.op_injective : ∀ {α : Type u_1}, Function.Injective AddOpposite.op
The theorem `AddOpposite.op_injective` states that for all types `α`, the function `AddOpposite.op` is injective. In other words, if `AddOpposite.op` applied to two elements of the type `α` produces the same result, then the two elements must be the same. This function `AddOpposite.op` essentially takes an element from a type and represents it in its additive opposite type. Therefore, the theorem guarantees that every element of the type `α` has a unique representation in its additive opposite type.
More concisely: For any type `α`, the function `AddOpposite.op` from `α` to its additive opposite type is an injection.
|
MulOpposite.op_zero
theorem MulOpposite.op_zero : ∀ {α : Type u_1} [inst : Zero α], MulOpposite.op 0 = 0
The theorem `MulOpposite.op_zero` states that for any type `α` that has a zero element (indicated by `[inst : Zero α]`), the "opposite" (under multiplication) of the zero element is itself. In other words, applying the `MulOpposite.op` function to zero yields zero. This is consistent with the mathematical principle that the additive identity (zero) is its own multiplicative opposite.
More concisely: For any type `α` with a zero element, `MulOpposite.op (Zero α) = Zero α`.
|
AddOpposite.unop_injective
theorem AddOpposite.unop_injective : ∀ {α : Type u_1}, Function.Injective AddOpposite.unop
The theorem `AddOpposite.unop_injective` states that for every type `α`, the function `AddOpposite.unop` is injective. In other words, it asserts that for any type `α`, if `AddOpposite.unop x` equals `AddOpposite.unop y`, then `x` must be equal to `y`. This is essentially saying that the function `AddOpposite.unop` does not map different elements of the type `αᵃᵒᵖ` (the additive opposite of α) to the same element of `α`, ensuring the uniqueness of the pre-image for each element in the co-domain.
More concisely: For every type `α`, the function `AddOpposite.unop` from the additive opposite `αᵃᵒᵖ` to `α` is a injection.
|
MulOpposite.op_one
theorem MulOpposite.op_one : ∀ {α : Type u_1} [inst : One α], MulOpposite.op 1 = 1
This theorem states that for any type `α` which has a multiplicative identity element (denoted by `1`), the "opposite" or "mirror" of this identity element using the `MulOpposite.op` function is still the identity. In other words, if you take the multiplicative identity of `α` and apply the `MulOpposite.op` function to it, you will still get the identity element. This holds true for any type `α` that has a multiplicative identity.
More concisely: For any type `α` with a multiplicative identity element `1`, the multiplicative identity and its opposite `MulOpposite.op 1` are equal.
|