AddCommMagma.add_comm
theorem AddCommMagma.add_comm : ∀ {G : Type u} [self : AddCommMagma G] (a b : G), a + b = b + a
This theorem states that in a structure (specifically, a commutative additive magma), defined over some type `G`, the operation of addition is commutative. In more concrete terms, for any two elements `a` and `b` of this type, the order in which they are added does not matter: adding `a` to `b` yields the same result as adding `b` to `a`. This is a basic property of addition in many mathematical structures, such as numbers.
More concisely: In a commutative additive magma, addition is commutative, i.e., for all `a` and `b` in the magma, `a + b = b + a`.
|
neg_add_self
theorem neg_add_self : ∀ {G : Type u_1} [inst : AddGroup G] (a : G), -a + a = 0
This theorem states that for any type `G` that forms an additive group, the additive inverse (`-a`) of any element `a` in `G` added to `a` itself equals zero. In other words, it encapsulates the property of groups where the sum of an element and its negative (or additive inverse) is the zero element. This is one of the basic properties of all additive groups, and in mathematical notation, it would be simply written as `-a + a = 0` for any `a` in the group `G`.
More concisely: For any additive group `G` and element `a` in `G`, `-a + a = 0`.
|
neg_eq_of_add_eq_zero_right
theorem neg_eq_of_add_eq_zero_right : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, a + b = 0 → -a = b := by
sorry
This theorem states that for any type `G` that forms a subtraction monoid, given any two elements `a` and `b` of type `G`, if the sum of `a` and `b` equals zero, then the negative of `a` is equal to `b`. In mathematical terms, this corresponds to the property $-a = b$ for any $a, b$ in a mathematical structure with subtraction such that $a + b = 0$.
More concisely: For any subtraction monoid type `G` and elements `a, b` of type `G` with `a + b = 0`, it holds that `-a = b`.
|
inv_mul_cancel_left
theorem inv_mul_cancel_left : ∀ {G : Type u_1} [inst : Group G] (a b : G), a⁻¹ * (a * b) = b
This theorem, `inv_mul_cancel_left`, states that for any type `G` that forms a Group, for any elements `a` and `b` of that Group, multiplying the inverse of `a` with the result of `a` multiplied by `b` will yield `b`. In mathematical terms, it expresses the property that for any element `a` of a group, its inverse `a⁻¹` cancels out `a` on the left side of a multiplication.
More concisely: For any group `G` and elements `a, b` in `G`, `a⁻¹ * a * b = b`.
|
RightCancelMonoid.npow_succ
theorem RightCancelMonoid.npow_succ :
∀ {M : Type u} [self : RightCancelMonoid M] (n : ℕ) (x : M),
RightCancelMonoid.npow (n + 1) x = RightCancelMonoid.npow n x * x
This theorem is stating a property about the operation of raising an element of a right cancelable monoid to the power of a natural number. Specifically, for any right cancelable monoid `M`, any natural number `n`, and any element `x` of `M`, raising `x` to the power of `n + 1` is the same as raising `x` to the power of `n` and then multiplying the result by `x`. This aligns with the typical understanding of exponentiation where, for example, `x` to the power of 3 is the same as `x` to the power of 2 multiplied by `x`.
More concisely: For any right cancelable monoid `M`, `x` in `M`, and natural number `n`, `x^(n+1) = x^n * x`.
|
add_assoc
theorem add_assoc : ∀ {G : Type u_1} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
This theorem states that for any type `G` that forms an additive semigroup, the operation of addition (`+`) is associative. In other words, for any three elements `a`, `b`, and `c` of `G`, the sum of `a`, `b`, and `c` doesn't depend on how the elements are grouped: adding `a` and `b` together first and then adding `c` is the same as adding `a` to the result of adding `b` and `c` together. This is expressed mathematically as `a + b + c = a + (b + c)`.
More concisely: For any additive semigroup `G`, the operation `+` is associative, that is, `a + b + c = a + (b + c)` for all elements `a, b, c` of `G`.
|
AddLeftCancelMonoid.add_zero
theorem AddLeftCancelMonoid.add_zero : ∀ {M : Type u} [self : AddLeftCancelMonoid M] (a : M), a + 0 = a
This theorem states that zero is a right neutral element for addition in the context of an "AddLeftCancelMonoid". In other words, for any type `M` that has an `AddLeftCancelMonoid` structure (meaning, roughly, that it behaves like numbers under addition), adding zero to any element `a` of type `M` results in the same element `a`. Mathematically, it can be expressed as `a + 0 = a`.
More concisely: In an AddLeftCancelMonoid, the additive identity (zero) leaves other elements unchanged in addition. That is, for all elements `a` of a type `M` with an AddLeftCancelMonoid structure, `a + 0 = a`.
|
AddCommGroup.add_comm
theorem AddCommGroup.add_comm : ∀ {G : Type u} [self : AddCommGroup G] (a b : G), a + b = b + a
This theorem states that addition is commutative in any commutative additive group. In other words, for any type `G` that has the structure of a commutative additive group, if `a` and `b` are elements of `G`, then the result of adding `a` to `b` is the same as the result of adding `b` to `a`. In mathematical notation, this can be represented as `a + b = b + a` for all `a, b` in `G`.
More concisely: In any commutative additive group, the order of adding elements does not affect their sum. That is, for all `a, b` in a commutative additive group `G`, `a + b = b + a`.
|
add_comm
theorem add_comm : ∀ {G : Type u_1} [inst : AddCommMagma G] (a b : G), a + b = b + a
This theorem states that for any type `G` that forms an additive commutative magma (i.e., a set with a binary operation that is commutative), the operation `+` is commutative. In other words, for any elements `a` and `b` of this type `G`, the result of `a + b` is the same as `b + a`. It enforces the general principle that the order in which two elements are added does not change the outcome, which is a fundamental property of addition in commutative magmas.
More concisely: For any commutative additive magma `G`, the operation `+` is commutative, i.e., `a + b = b + a` for all `a, b` in `G`.
|
AddRightCancelMonoid.zero_add
theorem AddRightCancelMonoid.zero_add : ∀ {M : Type u} [self : AddRightCancelMonoid M] (a : M), 0 + a = a
This theorem states that zero is a left neutral element for addition in an additive right-cancelable monoid. Specifically, for all types `M` that have an instance of the `AddRightCancelMonoid` structure, adding zero from the left to any element `a` of `M` results in `a`. This essentially formalizes the idea that for any number `a`, `0 + a` is always equal to `a`.
More concisely: In an additive right-cancelable monoid, zero acts as a left identity for addition.
|
add_right_cancel
theorem add_right_cancel :
∀ {G : Type u_1} [inst : Add G] [inst_1 : IsRightCancelAdd G] {a b c : G}, a + b = c + b → a = c
This theorem, `add_right_cancel`, states that for any type `G` that is equipped with an addition operation and has the right cancellation property, if we have three elements `a`, `b`, and `c` in `G` such that `a + b` equals `c + b`, then `a` must equal `c`. In other words, if two sums are equal and they have the same right-hand addend, then their left-hand addends must be equal. This is the definition of the right cancellation property in an additive setting.
More concisely: If `a + b = c + b` in an additive type `G` with right cancellation property, then `a = c`.
|
LeftCancelMonoid.one_mul
theorem LeftCancelMonoid.one_mul : ∀ {M : Type u} [self : LeftCancelMonoid M] (a : M), 1 * a = a
This theorem states that for any type `M` that forms a `LeftCancelMonoid`, the number one acts as a left neutral element for multiplication. In other words, for any element `a` of the type `M`, multiplying `1` with `a` (in the order `1 * a`) always results in `a`. In mathematical notation, this might be written as ∀a ∈ M, 1 * a = a.
More concisely: For any type `M` that is a `LeftCancelMonoid`, the multiplicative identity `1` acts as a left identity element, that is, `1 * a = a` for all `a` in `M`.
|
AddRightCancelMonoid.nsmul_succ
theorem AddRightCancelMonoid.nsmul_succ :
∀ {M : Type u} [self : AddRightCancelMonoid M] (n : ℕ) (x : M),
AddRightCancelMonoid.nsmul (n + 1) x = AddRightCancelMonoid.nsmul n x + x
This theorem states that in the context of an `AddRightCancelMonoid` M, the function `nsmul` (which represents multiplication by a natural number) behaves as expected when multiplying by `(n + 1 : ℕ)`. Specifically, multiplying an element `x` of the monoid by `(n + 1)` is the same as multiplying `x` by `n` and then adding `x`. In mathematical terms, this is saying that for any `n` in natural numbers and for any `x` in `AddRightCancelMonoid` M, `(n + 1) * x = n * x + x`.
More concisely: For any `AddRightCancelMonoid` M and natural numbers `n` and `x`, `(n + 1) * x = n * x + x`.
|
CommMagma.IsLeftCancelMul.toIsCancelMul
theorem CommMagma.IsLeftCancelMul.toIsCancelMul :
∀ (G : Type u) [inst : CommMagma G] [inst_1 : IsLeftCancelMul G], IsCancelMul G
This theorem states that for any type `G` which is a `CommMagma`, if `G` satisfies the `IsLeftCancelMul` property (i.e., for any elements `a`, `b`, and `c` in `G`, if `a * b = a * c` implies `b = c`), then `G` also satisfies the `IsCancelMul` property (i.e., both left and right cancellation law hold: for any `a`, `b`, and `c` in `G`, if `a * b = a * c` implies `b = c` and if `b * a = c * a` implies `b = c`). Here, `*` denotes the binary operation of the `CommMagma`.
More concisely: If a commutative magma `G` satisfies the left cancellation property for its multiplication, then it satisfies both the left and right cancellation properties for multiplication.
|
coe_nat_zsmul
theorem coe_nat_zsmul : ∀ {G : Type u_1} [inst : SubNegMonoid G] (a : G) (n : ℕ), ↑n • a = n • a
This theorem, `coe_nat_zsmul`, is an alias of `natCast_zsmul`. It states that for any given type `G` that is a member of the `SubNegMonoid` class (i.e., the type `G` supports subtraction and unary negation operations), and for any element `a` of that type and any natural number `n`, the scalar multiplication of `a` by the coercion of `n` to `G` (`↑n • a`) is the same as the scalar multiplication of `a` by `n` (`n • a`).
More concisely: For any type `G` in `SubNegMonoid` and element `a` in `G`, the coercion of a natural number `n` to `G` multiplied by `a` is equal to the scalar multiplication of `a` by `n`. (i.e., `↑n • a = n • a`)
|
neg_zero
theorem neg_zero : ∀ {G : Type u_1} [inst : NegZeroClass G], -0 = 0
This theorem, `neg_zero`, states that for any type `G` that is a member of the `NegZeroClass`, the negation of zero equals zero. In mathematical terms, it means that if `G` has a negation operation and a zero element, then the negation of the zero element is equal to the zero element itself.
More concisely: For any type `G` in the `NegZeroClass`, the negation of its zero element is equal to the zero element itself.
|
DivInvMonoid.zpow_succ'
theorem DivInvMonoid.zpow_succ' :
∀ {G : Type u} [self : DivInvMonoid G] (n : ℕ) (a : G),
DivInvMonoid.zpow (Int.ofNat n.succ) a = DivInvMonoid.zpow (Int.ofNat n) a * a
This theorem states that in a division-inverse monoid `G`, for any natural number `n` and any element `a` from `G`, the operation of raising `a` to the power of `n + 1` is equivalent to raising `a` to the power of `n` and then multiplying the result by `a`. In other words, `a^(n+1) = a^n * a`. Here, the power operation is extended to integers, with positive powers representing repeated multiplication, and negative powers representing repeated division or multiplication by the inverse.
More concisely: In a division-inverse monoid `G`, for any element `a` and natural number `n`, `a^(n+1)` equals `a^n * a`.
|
LeftCancelMonoid.npow_zero
theorem LeftCancelMonoid.npow_zero :
∀ {M : Type u} [self : LeftCancelMonoid M] (x : M), LeftCancelMonoid.npow 0 x = 1
This theorem states that for any type `M` which has a structure of a `LeftCancelMonoid`, the operation of raising any element `x` of `M` to the power of `0` (as defined by the `npow` function in `LeftCancelMonoid`) will always result in the identity element `1` of the `LeftCancelMonoid`. This aligns with the mathematical intuition that any number raised to the power of zero equals one.
More concisely: For any `LeftCancelMonoid` `M` and `x` in `M`, `x ^ 0 = 1` where `^` is the `LeftCancelMonoid` operation and `1` is the identity element of `M`.
|
AddCancelCommMonoid.add_comm
theorem AddCancelCommMonoid.add_comm : ∀ {M : Type u} [self : AddCancelCommMonoid M] (a b : M), a + b = b + a := by
sorry
This theorem states that the operation of addition is commutative in an additive commutative cancellative monoid. In other words, for any two elements 'a' and 'b' of a set 'M' that forms an additive commutative cancellative monoid, the sum of 'a' and 'b' is the same as the sum of 'b' and 'a'. This means that the order in which elements are added does not affect the result.
More concisely: In an additive commutative cancellative monoid, the order of adding elements does not affect the sum. Therefore, for all elements 'a' and 'b', 'a + b' equals 'b + a'.
|
CommGroup.mul_comm
theorem CommGroup.mul_comm : ∀ {G : Type u} [self : CommGroup G] (a b : G), a * b = b * a
This theorem states that in a commutative group (denoted as `CommGroup`), multiplication operation is commutative. Specifically, for any two elements `a` and `b` from a given commutative group `G`, the result of multiplying `a` by `b` is the same as the result of multiplying `b` by `a`. In other words, `a * b` equals `b * a` for all `a` and `b` in `G`.
More concisely: In a commutative group, the multiplication operation is commutative, i.e., for all `a, b` in `G`, `a * b` equals `b * a`.
|
div_eq_mul_inv
theorem div_eq_mul_inv : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
This theorem states that for any given type `G` that has a `DivInvMonoid` structure, division of two elements `a` and `b` of `G` is equivalent to the multiplication of `a` with the inverse of `b`. Essentially, it expresses the standard relationship `a / b = a * (1 / b)` in terms of multiplication and inversion. This theorem ensures better unfolding of types and is a duplicate of the `DivInvMonoid.div_eq_mul_inv` theorem in Lean 4.
More concisely: For any type `G` with a `DivInvMonoid` structure, the division of two elements `a` and `b` is equivalent to the multiplication of `a` by the multiplicative inverse of `b`. (Or, `a / b = a * b^(-1)`)
|
AddZeroClass.zero_add
theorem AddZeroClass.zero_add : ∀ {M : Type u} [self : AddZeroClass M] (a : M), 0 + a = a
This theorem states that zero is a left neutral element for addition. Specifically, for any type `M` that belongs to the `AddZeroClass`, when zero is added to any element `a` of type `M` on the left side, the result is the original element `a`. This essentially describes one of the fundamental properties of addition in any numerical system, where adding zero to any number leaves the number unchanged.
More concisely: For any type `M` in the `AddZeroClass`, zero acts as a left identity for the addition operation on `M`, i.e., `0 + a = a` for all `a` in `M`.
|
DivInvMonoid.zpow_zero'
theorem DivInvMonoid.zpow_zero' : ∀ {G : Type u} [self : DivInvMonoid G] (a : G), DivInvMonoid.zpow 0 a = 1
The theorem `DivInvMonoid.zpow_zero'` states that for any type `G` that is a `DivInvMonoid`, the power operation of any element `a` of type `G` raised to the power of 0 is equal to 1. In mathematical terms, this corresponds to the property `a ^ 0 = 1` for any element `a` in the division inverse monoid.
More concisely: For any type `G` being a `DivInvMonoid` and any element `a` in `G`, `a ^ 0 = 1`.
|
left_inv_eq_right_inv
theorem left_inv_eq_right_inv : ∀ {M : Type u} [inst : Monoid M] {a b c : M}, b * a = 1 → a * c = 1 → b = c
This theorem states that for any given monoid `M` and elements `a`, `b`, and `c` of `M`, if the product of `b` and `a` equals the identity of the monoid and the product of `a` and `c` also equals the identity, then `b` and `c` must be the same. The monoid structure here ensures the associativity of the operation and existence of an identity element.
More concisely: If two elements `a` and `c` of a monoid `M` have `a` and `c` being the inverse of `b` respectively, then `b` and `c` are equal.
|
division_def
theorem division_def : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
This theorem, named `division_def`, states that for any type `G` that forms a `DivInvMonoid`, dividing an element `a` by another element `b` is the same as multiplying `a` by the inverse of `b`. In mathematical terms, it asserts that for all `a` and `b` in `G`, `a / b` equals `a * b⁻¹`. This theorem is an alias of `DivInvMonoid.div_eq_mul_inv` and helps in ensuring better type unfolding.
More concisely: For any type `G` that forms a `DivInvMonoid`, `a / b = a * b⁻¹` for all `a, b` in `G`.
|
AddCommMagma.IsRightCancelAdd.toIsLeftCancelAdd
theorem AddCommMagma.IsRightCancelAdd.toIsLeftCancelAdd :
∀ (G : Type u) [inst : AddCommMagma G] [inst_1 : IsRightCancelAdd G], IsLeftCancelAdd G
This theorem states that for any type `G` that has the structure of an `AddCommMagma` (that is, a type with a commutative and associative addition operation), if `G` satisfies the property of right-cancellativity (`IsRightCancelAdd`), then it also satisfies the property of left-cancellativity (`IsLeftCancelAdd`). In mathematical terms, this means that if for all `a`, `b`, and `c` in `G`, `a + b = a + c` implies `b = c` (right-cancellativity), then for all `a`, `b`, and `c` in `G`, `b + a = c + a` also implies `b = c` (left-cancellativity).
More concisely: If `G` is an AddCommMagma and satisfies right-cancellativity (IsRightCancelAdd), then it also has left-cancellativity (IsLeftCancelAdd). In other words, if `a + b = a + c` implies `b = c` in a commutative and associative additive structure `G`, then `b + a = c + a` also implies `b = c`.
|
AddRightCancelMonoid.nsmul_zero
theorem AddRightCancelMonoid.nsmul_zero :
∀ {M : Type u} [self : AddRightCancelMonoid M] (x : M), AddRightCancelMonoid.nsmul 0 x = 0
This theorem, named `AddRightCancelMonoid.nsmul_zero`, states that for any type `M` that has an `AddRightCancelMonoid` structure, multiplying any element `x` of type `M` by the natural number `0` using the `AddRightCancelMonoid.nsmul` function yields the additive identity `0` in `M`. This is analogous to the property in standard arithmetic where any number multiplied by zero equals zero.
More concisely: For any AddRightCancelMonoid `M` and element `x` in `M`, `x * 0` equals the additive identity of `M`.
|
IsLeftCancelAdd.add_left_cancel
theorem IsLeftCancelAdd.add_left_cancel :
∀ {G : Type u} [inst : Add G] [self : IsLeftCancelAdd G] (a b c : G), a + b = a + c → b = c
This theorem states that addition is left cancellative in a given type `G` that is equipped with an addition operation. This means that for any elements `a`, `b`, and `c` in `G`, if the sum of `a` and `b` equals the sum of `a` and `c`, then `b` must equal `c`. In other words, if the same value `a` is added to two possibly different values `b` and `c` resulting in equal sums, then `b` and `c` were indeed the same value.
More concisely: If `a` is an element in a type `G` with addition operation, then for all `b` and `c` in `G`, if `a + b = a + c`, then `b = c`.
|
IsRightCancelMul.mul_right_cancel
theorem IsRightCancelMul.mul_right_cancel :
∀ {G : Type u} [inst : Mul G] [self : IsRightCancelMul G] (a b c : G), a * b = c * b → a = c
This theorem states that multiplication is right cancellative in a given type `G` that has a multiplication operation. This means that for any three elements `a`, `b`, and `c` in `G`, if the product of `a` and `b` is equal to the product of `c` and `b`, then `a` must be equal to `c`. This property allows for the cancellation of common factors on the right side of an equation.
More concisely: If `a * b = c * b` in type `G` with multiplication operation, then `a = c`.
|
add_left_neg
theorem add_left_neg : ∀ {G : Type u_1} [inst : AddGroup G] (a : G), -a + a = 0
This theorem states that for any type `G` that forms an additive group, the addition of an element `a` and its negative `-a` results in the additive identity `0`. In other words, for all elements `a` in the group, `-a + a = 0`. This is a formal statement of the property that every element in an additive group has an additive inverse.
More concisely: For every additive group `G` and element `a` in `G`, `-a + a = 0`.
|
LeftCancelMonoid.mul_one
theorem LeftCancelMonoid.mul_one : ∀ {M : Type u} [self : LeftCancelMonoid M] (a : M), a * 1 = a
This theorem asserts that one is a right neutral element for multiplication in the context of a left cancelable monoid. In other words, for any type `M` that has a structure of a `LeftCancelMonoid` (a monoid with the additional property that the operation of multiplication is left cancellable), and for any element `a` of type `M`, the result of multiplying `a` by one is `a`. This mirrors the familiar property from arithmetic where any number multiplied by one remains the same.
More concisely: In a left cancelable monoid, the multiplicative identity element acts as a right identity for every element.
|
SubtractionCommMonoid.add_comm
theorem SubtractionCommMonoid.add_comm : ∀ {G : Type u} [self : SubtractionCommMonoid G] (a b : G), a + b = b + a := by
sorry
This theorem states that addition is a commutative operation in a subtraction-commutative monoid. In other words, for any type `G` that has a structure of a `SubtractionCommMonoid` (a mathematical structure equipped with an addition and a subtraction operation that are both commutative), given any two elements `a` and `b` from `G`, the result of `a + b` is the same as the result of `b + a`.
More concisely: In a subtraction-commutative monoid, the addition operation is commutative. Therefore, for all elements `a` and `b`, `a + b = b + a`.
|
inv_mul_self
theorem inv_mul_self : ∀ {G : Type u_1} [inst : Group G] (a : G), a⁻¹ * a = 1
This theorem, `inv_mul_self`, states that for any type `G` that forms a group, the multiplicative inverse of any element `a` from `G` when multiplied with `a` itself yields the multiplicative identity `1`. In mathematical terms, this represents the property ∀a ∈ G, a⁻¹ * a = 1, which holds true for all groups.
More concisely: For all groups G and all its elements a, a^-1 * a = 1.
|
sub_eq_add_neg
theorem sub_eq_add_neg : ∀ {G : Type u_1} [inst : SubNegMonoid G] (a b : G), a - b = a + -b
This theorem states that in any Subtraction-Negative Monoid (`SubNegMonoid`), denoted by `G`, subtracting an element `b` from another element `a` is equivalent to adding the negative of `b` to `a`. In other words, for any elements `a` and `b` in `G`, the expression `a - b` is the same as `a + -b`. This theorem is a duplicate of `SubNegMonoid.sub_eq_mul_neg` but is written in a way that ensures the types unfold better.
More concisely: In any Subtraction-Negative Monoid, for all elements `a` and `b`, `a - b` equals `a + (-b)`.
|
neg_add_cancel_left
theorem neg_add_cancel_left : ∀ {G : Type u_1} [inst : AddGroup G] (a b : G), -a + (a + b) = b
This theorem, `neg_add_cancel_left`, states that for any type `G` that is an additive group, and for any two elements `a` and `b` of this type `G`, the result of adding the additive inverse of `a` to the sum of `a` and `b` is always equal to `b`. In mathematical terms, it states that for all `a` and `b` in an additive group, `-a + (a + b) = b`. This is essentially an application of the additive inverse property in group theory.
More concisely: For all additive groups `G`, and elements `a` and `b` in `G`, the additive inverse of `a` combined with `a` and `b` equals `b`, i.e., `-a + (a + b) = b`.
|
inv_eq_of_mul_eq_one_right
theorem inv_eq_of_mul_eq_one_right : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, a * b = 1 → a⁻¹ = b := by
sorry
This theorem states that for any type `G` that forms a Division Monoid (a set with a binary operation, an identity element, and an inverse for each element), given two elements `a` and `b` from `G`, if the product of `a` and `b` equals the identity element `1`, then the inverse of `a` is equal to `b`. In mathematical terms, for any elements `a`, `b` of a division monoid `G`, if `a * b = 1`, then `a⁻¹ = b`.
More concisely: In a division monoid, if the product of two elements equals the identity, then they are inverses of each other.
|
neg_neg
theorem neg_neg : ∀ {G : Type u_1} [inst : InvolutiveNeg G] (a : G), - -a = a
This theorem, `neg_neg`, states that for any type within an `InvolutiveNeg` typeclass, the double negation of an element is equivalent to the element itself. In other words, given a type `G` that has an `InvolutiveNeg` instance and any element `a` of that type `G`, applying the negation operation twice (`- -a`) results in the original element `a`. This follows the mathematical principle that the double negation of a number is the number itself.
More concisely: For any type `G` with an `InvolutiveNeg` instance, `-- a = a` holds for all elements `a` of `G`.
|
inv_one
theorem inv_one : ∀ {G : Type u_1} [inst : InvOneClass G], 1⁻¹ = 1
This theorem, `inv_one`, states that for any given type `G` with an instance of the `InvOneClass` (meaning `G` has definitions for inversion and the number one), the inverse of one is always equal to one. This is a general property that holds in many mathematical structures, such as groups, fields, and rings where the element "one" is defined and has an inverse. In Layman's terms, turning one upside down (or taking its inverse) still gives you one.
More concisely: For any type `G` with an `InvOneClass`, the inverse of `1` in `G` equals `1`.
|
inv_inv
theorem inv_inv : ∀ {G : Type u_1} [inst : InvolutiveInv G] (a : G), a⁻¹⁻¹ = a
This theorem states that for any type `G` that has an involutive inverse property (that is, the inverse operation is its own inverse), the double inverse of any element `a` of `G` is equal to `a` itself. In mathematical terms, for all `a` in `G`, (a⁻¹)⁻¹ = a.
More concisely: For any type `G` with involutive inverses, the double inverse of any element `a` equals `a` itself: (a⁻¹)⁻¹ = a.
|
AddCommMagma.IsLeftCancelAdd.toIsCancelAdd
theorem AddCommMagma.IsLeftCancelAdd.toIsCancelAdd :
∀ (G : Type u) [inst : AddCommMagma G] [inst_1 : IsLeftCancelAdd G], IsCancelAdd G
This theorem states that for any type `G` that forms an additive commutative magma (i.e., it has an operation that is associative and commutative), if this type `G` also satisfies the property of being left-cancellative under addition (that is, for all `a`, `b` and `c` in `G`, if `a + b = a + c` then `b = c`), then `G` necessarily satisfies the property of being cancellative under addition. In the latter property, the cancellation can happen on either side, meaning that if `a + b = c + b` then `a = c`, and if `b + a = b + c` then `a = c`.
More concisely: If `G` is an additive commutative magma that is left-cancelled under addition, then `G` is cancellative under addition (i.e., for all `a`, `b`, `c` in `G`, if `a + b = c + b` then `a = c` and if `b + a = b + c` then `a = c`).
|
AddCommMagma.IsLeftCancelAdd.toIsRightCancelAdd
theorem AddCommMagma.IsLeftCancelAdd.toIsRightCancelAdd :
∀ (G : Type u) [inst : AddCommMagma G] [inst_1 : IsLeftCancelAdd G], IsRightCancelAdd G
This theorem states that for any type `G` that is an instance of `AddCommMagma` (meaning it has an associative and commutative addition operation), if `G` satisfies the property `IsLeftCancelAdd` (where for any three elements `a`, `b`, and `c` in `G`, `a + b = a + c` implies `b = c`), then it also satisfies the property `IsRightCancelAdd` (where for any three elements `a`, `b`, and `c` in `G`, `b + a = c + a` implies `b = c`). Simply put, if addition on the left can cancel elements in `G`, then addition on the right can also cancel elements in `G`.
More concisely: If `G` is an associative and commutative type satisfying the left cancellation property for addition, then `G` also satisfies the right cancellation property for addition.
|
left_neg_eq_right_neg
theorem left_neg_eq_right_neg : ∀ {M : Type u} [inst : AddMonoid M] {a b c : M}, b + a = 0 → a + c = 0 → b = c := by
sorry
This theorem states that for any type `M` which is an additive monoid and any three elements `a`, `b`, and `c` of type `M`, if the sum of `b` and `a` is zero, and the sum of `a` and `c` is also zero, then `b` must be equal to `c`. In other words, if two different pairs of elements from the monoid add up to zero and they share a common element, that common element acts as a sort of "balancer" causing the other elements in the pairs to be equal. This is a property specific to the structure of additive monoids.
More concisely: In an additive monoid, if the sum of two elements is zero with a common element, then the elements are equal.
|
CommMonoid.mul_comm
theorem CommMonoid.mul_comm : ∀ {M : Type u} [self : CommMonoid M] (a b : M), a * b = b * a
This theorem states that for any type `M` that forms a commutative monoid, the multiplication operation is commutative. In other words, for any two elements `a` and `b` of type `M`, the result of multiplying `a` by `b` is the same as the result of multiplying `b` by `a`. This is a specific instance of the general principle that in a commutative monoid (a set equipped with an associative binary operation that has an identity element and in which the operation is commutative), the order of multiplication does not matter.
More concisely: In a commutative monoid, the multiplication operation is commutative, i.e., for all elements a and b, a * b = b * a.
|
inv_mul_cancel_right
theorem inv_mul_cancel_right : ∀ {G : Type u_1} [inst : Group G] (a b : G), a * b⁻¹ * b = a
This theorem states that for any group `G` and any elements `a` and `b` of that group, if you multiply `a` by the inverse of `b` and then by `b` itself, you get back `a`. This is a property of group theory where the multiplication of an element and its inverse gives the identity element, so multiplying by the inverse and the element itself is effectively doing nothing. In mathematical terms, this theorem establishes that `a * b⁻¹ * b = a` for all `a` and `b` in any group `G`.
More concisely: For all groups G, elements a and b in G, a * b⁻¹ * b = a.
|
neg_add_cancel_comm
theorem neg_add_cancel_comm : ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), -a + b + a = b
This theorem, `neg_add_cancel_comm`, states that for any type `G` equipped with the structure of an additive commutative group, for any two elements `a` and `b` of this group, the sum of the negation of `a`, `b`, and `a` is equal to `b`. In mathematical terms, for any `a` and `b` in some additive commutative group `G`, we have that `-a + b + a = b`. This result is a reflection of the property of additive inverses in a commutative group.
More concisely: For any additive commutative group `G` and elements `a, b` in `G`, we have `-a + b + a = b`.
|
AddMonoid.add_zero
theorem AddMonoid.add_zero : ∀ {M : Type u} [self : AddMonoid M] (a : M), a + 0 = a
This theorem states that zero acts as a right neutral element for the operation of addition in an additive monoid. In other words, for any object `a` of type `M` that forms an additive monoid, adding zero to `a` (i.e., `a + 0`) results in `a` itself. This is a fundamental property of addition in mathematical structures such as groups and rings, expressed here in the context of a general additive monoid.
More concisely: For any additive monoid `M` and object `a` in `M`, `a + 0 = a`.
|
pow_zero
theorem pow_zero : ∀ {M : Type u_2} [inst : Monoid M] (a : M), a ^ 0 = 1
This theorem, `pow_zero`, states that for any type `M` that forms a monoid (a set equipped with an associative binary operation and an identity element), raising any element `a` of `M` to the power of zero results in the identity element of the monoid. In other words, for any `a` in a monoid `M`, `a` to the power of zero equals one. This mirrors the familiar property from mathematics where any nonzero number raised to the power of zero equals one.
More concisely: For any monoid `M` and element `a` in `M`, `a^0 = id`, where `id` is the identity element of the monoid.
|
AddRightCancelMonoid.add_zero
theorem AddRightCancelMonoid.add_zero : ∀ {M : Type u} [self : AddRightCancelMonoid M] (a : M), a + 0 = a
This theorem states that zero is the right neutral element for addition in an additive right cancel monoid. Specifically, for any type `M` that has an `AddRightCancelMonoid` structure, adding zero to any element `a` of `M` will result in the same element `a`. In mathematical notation, this is equivalent to saying for any `a` in `M`, `a + 0 = a`.
More concisely: In an additive right cancel monoid, zero is the right identity for addition.
|
AddCommSemigroup.add_comm
theorem AddCommSemigroup.add_comm : ∀ {G : Type u} [self : AddCommSemigroup G] (a b : G), a + b = b + a
This theorem states that addition is commutative in an additive commutative semigroup. In more detail, for any given type `G` that is an additive commutative semigroup, and for any two elements `a` and `b` of type `G`, the result of `a + b` is equal to the result of `b + a`. This is a fundamental property of additive commutative semigroups, which are algebraic structures consisting of a set equipped with an associative addition operation that is also commutative.
More concisely: In an additive commutative semigroup, adding any two elements is commutative. (i.e., `a + b = b + a` for all `a, b` in the semigroup.)
|
zero_zsmul
theorem zero_zsmul : ∀ {G : Type u_1} [inst : SubNegMonoid G] (a : G), 0 • a = 0
This theorem states that, for any type `G` that is a `SubNegMonoid` (a structure with subtraction and negation operations), the scalar multiplication of zero (`0`) and any element `a` from `G` will always yield zero (`0`). This is a generalization of the standard algebraic property that multiplying anything by zero gives zero, but in the context of any object that behaves like numbers with respect to subtraction and negation.
More concisely: For any type `G` with subtraction and negation operations, scalar multiplication of any element `a` in `G` by zero results in zero.
|
DivisionCommMonoid.mul_comm
theorem DivisionCommMonoid.mul_comm : ∀ {G : Type u} [self : DivisionCommMonoid G] (a b : G), a * b = b * a
This theorem states that in a division commutative monoid `G`, the operation of multiplication is commutative. That is, for any two elements `a` and `b` in `G`, the result of multiplying `a` by `b` is the same as the result of multiplying `b` by `a`.
More concisely: In a commutative monoid `G`, multiplication of elements `a` and `b` is commutative: `a * b = b * a`.
|
mul_left_cancel
theorem mul_left_cancel :
∀ {G : Type u_1} [inst : Mul G] [inst_1 : IsLeftCancelMul G] {a b c : G}, a * b = a * c → b = c
This theorem, `mul_left_cancel`, states that in any type `G` equipped with a multiplication operation (`Mul G`) and the property that multiplication is left-cancellable (`IsLeftCancelMul G`), for any elements `a`, `b`, `c` of `G`, if the equation `a * b = a * c` holds, then `b` must equal `c`. In other words, if you multiply the same value `a` by two different values `b` and `c` and get the same result, then `b` and `c` must have been the same to begin with, as long as the multiplication operation is left-cancellable in the system you're working within.
More concisely: If `a` is an element of a group `G` with left-cancellative multiplication, then `b = c` given `a * b = a * c`.
|
DivInvMonoid.zpow_neg'
theorem DivInvMonoid.zpow_neg' :
∀ {G : Type u} [self : DivInvMonoid G] (n : ℕ) (a : G),
DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
The theorem `DivInvMonoid.zpow_neg'` states that for any given type `G` that forms a division and inverse monoid and any element `a` of type `G` and natural number `n`, the negated successor of `n`, when used as the exponent of `a` in the power operation, is equivalent to the inverse of `a` raised to the power of the successor of `n`. In mathematical terms, this can be written as `a ^ -(n + 1) = (a ^ (n + 1))⁻¹`.
More concisely: For any division and inverse monoid `G` and its element `a` and natural number `n`, `a^(-(n+1)) = (a^(n+1))^-1`.
|
succ_nsmul
theorem succ_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (n : ℕ), (n + 1) • a = n • a + a
This theorem, named `succ_nsmul`, applies to any type `M` that forms an additive monoid. It takes an element `a` of type `M` and a natural number `n`, and states that scaling `a` by `n + 1` (denoted `(n + 1) • a`) is the same as scaling `a` by `n` and then adding `a` (denoted `n • a + a`). This is a generalization of the arithmetic fact that `(n + 1) * a = n * a + a`.
More concisely: For all additive monoids M, (n + 1) • a = n • a + a, where • denotes scaling and + denotes addition.
|
zero_nsmul
theorem zero_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M), 0 • a = 0
This theorem states that for any type `M` that is an additive monoid, the scalar multiplication of any element `a` from `M` by zero equals the additive identity element (0) of `M`. In other words, multiplying any element of an additive monoid by zero always results in zero. This is a common property in many algebraic structures such as numbers, vectors, matrices, etc.
More concisely: For any additive monoid M and element a in M, a * 0 = 0.
|
add_right_cancel_iff
theorem add_right_cancel_iff :
∀ {G : Type u_1} [inst : Add G] [inst_1 : IsRightCancelAdd G] {a b c : G}, b + a = c + a ↔ b = c
This theorem states that for any type `G` that has an addition operation and the right cancellation property, given any three elements `a`, `b`, and `c` of type `G`, the equation `b + a = c + a` is equivalent to `b = c`. In other words, adding the same element `a` to two elements `b` and `c` in an additive group with right cancelability, if the results are equal, then the original elements `b` and `c` must have been equal to begin with.
More concisely: In an additive group with right cancellation, if `a`, `b`, and `c` are elements such that `b + a = c + a`, then `b = c`.
|
mul_comm
theorem mul_comm : ∀ {G : Type u_1} [inst : CommMagma G] (a b : G), a * b = b * a
This theorem states that for any type `G` that forms a commutative magma (denoted as `CommMagma G`), the multiplication operation is commutative. In other words, for any two elements `a` and `b` of type `G`, the product of `a` and `b` (`a * b`) is equal to the product of `b` and `a` (`b * a`). This is a formalization of the commutative property of multiplication, which is familiar from elementary algebra.
More concisely: For any commutative magma `G`, the multiplication operation is commutative, i.e., `a * b = b * a` for all `a, b` in `G`.
|
add_neg_cancel_left
theorem add_neg_cancel_left : ∀ {G : Type u_1} [inst : AddGroup G] (a b : G), a + (-a + b) = b
This theorem states that for any type `G` that has the structure of an add group, for any elements `a` and `b` of `G`, adding `a` to the result of adding the negation of `a` to `b` will always equal `b`. In mathematical terms, it says that for any elements `a` and `b` in an additive group, the equation `a + (-a + b) = b` always holds, demonstrating the cancellation property of the negation in the group.
More concisely: For any add group `G` and elements `a, b` in `G`, `a + (-a + b) = b`.
|
CommMagma.IsRightCancelMul.toIsCancelMul
theorem CommMagma.IsRightCancelMul.toIsCancelMul :
∀ (G : Type u) [inst : CommMagma G] [inst_1 : IsRightCancelMul G], IsCancelMul G
This theorem states that for any type `G` which forms a Commutative Magma (i.e., it has an associative binary operation that is commutative), if the property of right-cancellativity holds (i.e., for any elements `a`, `b` and `c` in `G`, if `a * c = b * c`, then `a = b`), then the property of cancellativity also holds in both directions (i.e., for any elements `a`, `b` and `c` in `G`, if `a * b = a * c` then `b = c` and if `b * a = c * a` then `b = c`).
More concisely: In a commutative magma where right-cancellativity holds, cancellativity holds in both directions.
|
add_left_cancel
theorem add_left_cancel :
∀ {G : Type u_1} [inst : Add G] [inst_1 : IsLeftCancelAdd G] {a b c : G}, a + b = a + c → b = c
The theorem `add_left_cancel` states that for any type `G` that has an addition operation and also has the property of left-cancellativity under addition, if `a`, `b`, and `c` are of type `G`, then if `a + b` equals `a + c`, it implies that `b` equals `c`. In other words, in an algebraic structure where addition is defined and is left-cancellable, adding the same quantity to two quantities and getting equal results means the original quantities were equal.
More concisely: In a left-cancellative group, if `a + b = a + c`, then `b = c`.
|
zero_add
theorem zero_add : ∀ {M : Type u} [inst : AddZeroClass M] (a : M), 0 + a = a
This theorem, named `zero_add`, states that for any type `M` that forms an additive zero class (i.e., it has a zero element and an addition operation), adding zero to any element `a` of type `M` will yield `a` itself. This is a restatement of one of the fundamental properties of additive identity, expressed in the context of type theory.
More concisely: For any additive type `M` and element `a` in `M`, `a + 0 = a`.
|
add_neg_cancel_right
theorem add_neg_cancel_right : ∀ {G : Type u_1} [inst : AddGroup G] (a b : G), a + b + -b = a
This theorem, `add_neg_cancel_right`, states that for any type `G` that has an addition group structure (denoted by `AddGroup G`), for any two instances `a` and `b` of that type, if we add `b` to `a` and then add the additive inverse of `b` (notated as `-b`), we get `a` back. In other words, adding an element and its negation in an additive group cancels out, leaving the original element — this is a fundamental property of groups. In common mathematical notation, this would be expressed as \(a + b + (-b) = a\).
More concisely: For any additive group `G` and elements `a` and `b` in `G`, `a + b + (-b) = a`.
|
inv_eq_of_mul_eq_one_left
theorem inv_eq_of_mul_eq_one_left : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, a * b = 1 → b⁻¹ = a := by
sorry
This theorem states that for any type `G` that has a division monoid structure, given any two elements `a` and `b` of type `G`, if the multiplication of `a` and `b` equals to the identity element `1`, then the multiplicative inverse of `b` is equal to `a`. In mathematical terms, for all `a` and `b` in a division monoid, if `a * b = 1`, then `b⁻¹ = a`.
More concisely: If `a` and `b` are elements of a division monoid such that `a * b = 1`, then `b` is the multiplicative inverse of `a`, i.e., `b⁻¹ = a`.
|
mul_assoc
theorem mul_assoc : ∀ {G : Type u_1} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
This theorem is about the associativity of multiplication in a semigroup. For any semigroup `G` and any three elements `a`, `b`, and `c` of `G`, the operation of multiplication is associative. In other words, the order in which the multiplication operations are performed does not affect the result: `(a * b) * c` is the same as `a * (b * c)`.
More concisely: In any semigroup, the multiplication is associative: `(a * b) * c = a * (b * c)` for all elements `a`, `b`, and `c`.
|
MulOneClass.mul_one
theorem MulOneClass.mul_one : ∀ {M : Type u} [self : MulOneClass M] (a : M), a * 1 = a
The theorem `MulOneClass.mul_one` states that for any type `M` that has a multiplication operation and a distinct element defined as one (`1`), multiplication of any element `a` of type `M` with `1` results in `a` itself. In mathematical terms, it asserts for all `a` in a multiplication-one class `M`, `a * 1 = a`. This is a formal way of stating the property that `1` is the right neutral element for the multiplication operation in a semi-group or a group.
More concisely: For any multiplication-one class `M` with identity `1`, multiplication by `1` is the identity function. That is, for all `a` in `M`, `a * 1 = a`.
|
RightCancelMonoid.npow_zero
theorem RightCancelMonoid.npow_zero :
∀ {M : Type u} [self : RightCancelMonoid M] (x : M), RightCancelMonoid.npow 0 x = 1
The theorem `RightCancelMonoid.npow_zero` states that for any given type `M` that has a `RightCancelMonoid` structure, raising any element `x` of `M` to the power of zero (denoted as `(0 : ℕ)`) is equal to `1`. This is a property of `RightCancelMonoid` in the context of natural numbers. More formally, it can be written in mathematical notation as follows: for any `x` in `M`, `x^0 = 1`, where `^` denotes the operation of the right-cancel monoid.
More concisely: For any right-cancel monoid `M` and element `x` in `M`, `x^0 = 1`.
|
AddZeroClass.add_zero
theorem AddZeroClass.add_zero : ∀ {M : Type u} [self : AddZeroClass M] (a : M), a + 0 = a
This theorem states that zero is a right neutral element for addition. In other words, for any type `M` that is an instance of the `AddZeroClass` (which means it has a zero element and an addition operation), adding zero to any element `a` of `M` will result in `a` itself. This corresponds to the familiar fact from basic algebra that adding zero to any number does not change the value of the number.
More concisely: For any type `M` with zero element `0` and addition operation `+`, `a + 0 = a` for all `a` in `M`.
|
AddSemigroup.add_assoc
theorem AddSemigroup.add_assoc : ∀ {G : Type u} [self : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
The theorem `AddSemigroup.add_assoc` states that addition is associative in any add semigroup. More specifically, for any type `G` that has an `AddSemigroup` structure, and any elements `a`, `b`, and `c` of `G`, the sum of `a`, `b`, and `c` is the same whether you first add `a` and `b` and then add `c`, or first add `b` and `c` and then add to `a`. In mathematical notation, this is expressed as `a + b + c = a + (b + c)`.
More concisely: For any add semigroup `G` and elements `a`, `b`, `c` in `G`, `a + (b + c) = (a + b) + c`.
|
add_right_neg
theorem add_right_neg : ∀ {G : Type u_1} [inst : AddGroup G] (a : G), a + -a = 0
This theorem states that for any type `G` that forms an additive group, adding any element `a` of type `G` to its additive inverse `-a` results in the additive identity `0`. This is a fundamental property of all additive groups, denoted mathematically as `a + (-a) = 0` for all `a` in the group.
More concisely: For any additive group `G` and element `a` in `G`, `a + (-a) = 0`.
|
add_left_cancel_iff
theorem add_left_cancel_iff :
∀ {G : Type u_1} [inst : Add G] [inst_1 : IsLeftCancelAdd G] {a b c : G}, a + b = a + c ↔ b = c
This theorem states that for any type `G` which has a defined addition operation and possesses the left cancellation property under addition, given any three elements `a`, `b`, and `c` of `G`, the statement `a + b = a + c` is equivalent to `b = c`. In other words, the addition operation is left-cancellable in `G`: if adding `a` to `b` results in the same value as adding `a` to `c`, then `b` must be equal to `c`.
More concisely: For any type `G` with left-cancellative addition operation, `a + b = a + c` implies `b = c`.
|
CommSemigroup.mul_comm
theorem CommSemigroup.mul_comm : ∀ {G : Type u} [self : CommSemigroup G] (a b : G), a * b = b * a
This theorem states that for any type `G` that has a `CommSemigroup` structure, multiplication is commutative. That is, for any two elements `a` and `b` of type `G`, the result of `a` multiplied by `b` is the same as `b` multiplied by `a`. This is a property of a structure known as a commutative semigroup, where the multiplication operation is both associative and commutative.
More concisely: For any type `G` with a `CommSemigroup` structure, multiplication is commutative, i.e., `a * b = b * a` for all `a, b` in `G`.
|
eq_inv_of_mul_eq_one_left
theorem eq_inv_of_mul_eq_one_left : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, a * b = 1 → a = b⁻¹ := by
sorry
This theorem, `eq_inv_of_mul_eq_one_left`, states that for any type `G` that is a division monoid, given any two elements `a` and `b` of this type, if the product of `a` and `b` equals one (`1`), then `a` must be the multiplicative inverse of `b` (notated as `b⁻¹`). In other words, in a division monoid, if two elements multiply to give the multiplicative identity, then each element is the multiplicative inverse of the other.
More concisely: In a division monoid, if `a` and `b` are elements such that `a * b = 1`, then `a` is the multiplicative inverse of `b`, i.e., `a = b⁻¹`.
|
one_mul
theorem one_mul : ∀ {M : Type u} [inst : MulOneClass M] (a : M), 1 * a = a
This theorem states that for any type `M` that has a multiplication operation and a defined element '1' (i.e., `M` is an instance of `MulOneClass`), the product of '1' and any element `a` of type `M` is just `a` itself. In other words, '1' acts as a multiplicative identity in the type `M`. In mathematical terms, for any element `a` in `M`, the equation `1 * a = a` holds true.
More concisely: For any type `M` instancing `MulOneClass` with multiplicative identity '1', the equation `1 * a = a` holds for all `a` in `M`.
|
AddMonoid.nsmul_zero
theorem AddMonoid.nsmul_zero : ∀ {M : Type u} [self : AddMonoid M] (x : M), AddMonoid.nsmul 0 x = 0
The theorem `AddMonoid.nsmul_zero` states that for any type `M` that has an `AddMonoid` structure, multiplying any element `x` of `M` by the natural number `0` (using the `nsmul` function provided by the `AddMonoid` structure) results in the additive identity (`0`) of the `AddMonoid`. In mathematical terms, this ensures that multiplying any element in our additive monoid by zero always yields the zero element, a property that is expected in a mathematical structure like a monoid.
More concisely: For any AddMonoid M and its zero element 0, for all x in M, x⊝0 = 0. (Here, ⊝ represents the `nsmul` function in Lean.)
|
AddLeftCancelMonoid.nsmul_zero
theorem AddLeftCancelMonoid.nsmul_zero :
∀ {M : Type u} [self : AddLeftCancelMonoid M] (x : M), AddLeftCancelMonoid.nsmul 0 x = 0
The theorem `AddLeftCancelMonoid.nsmul_zero` states that for any given type `M` that has the structure of an `AddLeftCancelMonoid`, the "multiplication" operation (`nsmul`), when applied with `0` and any element `x` of type `M`, will return `0`. In other words, `nsmul 0 x` is equal to `0` for any `x` in an `AddLeftCancelMonoid`. This is analogous to the multiplication property in regular arithmetic where any number multiplied by zero equals zero.
More concisely: For any AddLeftCancelMonoid `M`, `nsmul 0 x = 0` for all `x` in `M`.
|
negSucc_zsmul
theorem negSucc_zsmul : ∀ {G : Type u_2} [inst : SubNegMonoid G] (a : G) (n : ℕ), Int.negSucc n • a = -((n + 1) • a)
The theorem `negSucc_zsmul` states that for any type `G` that is a subtraction-negative monoid (i.e., a mathematical structure with subtraction and negation operations), and for any element `a` of this type and any natural number `n`, the scalar multiplication of `a` by the negative successor of `n` (i.e., `Int.negSucc n • a`) is equal to the negation of the scalar multiplication of `a` by `n + 1` (i.e., `-((n + 1) • a)`). In other words, scalar multiplication by a negative integer in this structure mirrors scalar multiplication by the corresponding positive integer, followed by negation.
More concisely: For any subtraction-negative monoid type `G` and element `a` in `G`, `Int.negSucc n • a = -(n + 1 • a)`.
|
mul_inv_self
theorem mul_inv_self : ∀ {G : Type u_1} [inst : Group G] (a : G), a * a⁻¹ = 1
This theorem states that for any element 'a' in a group 'G', the product of 'a' and its inverse 'a⁻¹' equals the identity element '1'. This is a fundamental property of groups in abstract algebra, where every element has an inverse such that multiplying the element and its inverse always gives the identity element.
More concisely: In a group, the product of any element and its inverse is the identity element.
|
CancelCommMonoid.mul_comm
theorem CancelCommMonoid.mul_comm : ∀ {M : Type u} [self : CancelCommMonoid M] (a b : M), a * b = b * a
This theorem states that the multiplication operation is commutative in a commutative multiplicative magma. In other words, for any type `M` that has a structure of `CancelCommMonoid`, and for any two elements `a` and `b` of this type, the result of multiplying `a` by `b` is the same as the result of multiplying `b` by `a`. A `CancelCommMonoid` is a mathematical structure where multiplication is associative, commutative, and cancellative.
More concisely: In a commutative magma with a `CancelCommMonoid` structure, multiplication of elements is commutative.
|
CommMagma.IsRightCancelMul.toIsLeftCancelMul
theorem CommMagma.IsRightCancelMul.toIsLeftCancelMul :
∀ (G : Type u) [inst : CommMagma G] [inst_1 : IsRightCancelMul G], IsLeftCancelMul G
This theorem states that for any type `G` that is a Commutative Magma (denoted as `CommMagma G`), if `G` additionally satisfies the property of right cancellation for multiplication (expressed as `IsRightCancelMul G`), then `G` will also satisfy the property of left cancellation for multiplication (resulting in `IsLeftCancelMul G`). In mathematical terms, if for all `a`, `b`, and `c` in `G`, the equation `a * b = a * c` implies `b = c`, then it also holds that `a * b = c * b` implies `a = c`.
More concisely: If `G` is a commutative magma with right cancellation for multiplication, then `G` has left cancellation for multiplication.
|
zpow_coe_nat
theorem zpow_coe_nat : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a : G) (n : ℕ), a ^ ↑n = a ^ n
This is a theorem about exponentiation in a division and inversion monoid (a type of mathematical structure). This theorem states that for any element `a` of type `G` (where `G` is a division and inversion monoid) and any natural number `n`, raising `a` to the power of the coercion of `n` to an integer is the same as raising `a` to the power of `n`. In other words, it doesn't matter whether we treat `n` as a natural number or an integer when doing exponentiation in this context.
More concisely: For any division and inversion monoid `G` and any natural number `n`, the exponentiation `a ^ (coe n)` is equal to `a ^ n`, where `a` is an element of `G`.
|
AddCommMonoid.add_comm
theorem AddCommMonoid.add_comm : ∀ {M : Type u} [self : AddCommMonoid M] (a b : M), a + b = b + a
This theorem states that addition is commutative in any commutative additive monoid. In other words, for any two elements `a` and `b` of a given type `M` which forms a commutative additive monoid, the result of `a + b` will always be the same as the result of `b + a`. This is a fundamental property of addition in such algebraic structures.
More concisely: In a commutative additive monoid, the order of adding elements does not affect their sum. That is, for all `a` and `b` in the monoid `M`, `a + b = b + a`.
|
add_neg_self
theorem add_neg_self : ∀ {G : Type u_1} [inst : AddGroup G] (a : G), a + -a = 0
This theorem states that for any given type `G` equipped with the structure of an additive group, the sum of any element `a` and its additive inverse `-a` is always zero. In mathematical terms, it asserts the fundamental group property that each element plus its opposite equals the additive identity, which is zero in this context.
More concisely: For any additive group `G` and element `a` in `G`, `a + (-a) = 0`.
|
Monoid.one_mul
theorem Monoid.one_mul : ∀ {M : Type u} [self : Monoid M] (a : M), 1 * a = a
This theorem, named `Monoid.one_mul`, states that in any monoid `M`, the multiplicative identity (1) acts as a left neutral element. That is, for any element `a` of `M`, the product of 1 and `a` is just `a` itself. Mathematically, this can be written as: ∀a ∈ M, 1*a = a. This property is fundamental to the definition of a monoid, which is a set equipped with an associative binary operation and an identity element.
More concisely: In any monoid, the multiplicative identity element acts as a left identity for every other element.
|
RightCancelMonoid.mul_one
theorem RightCancelMonoid.mul_one : ∀ {M : Type u} [self : RightCancelMonoid M] (a : M), a * 1 = a
This theorem states that one is a right neutral element for multiplication in the context of a right cancelable monoid. This means that for any value `a` of type `M` (which is a right cancelable monoid), the result of multiplying `a` by 1 is `a` itself. In math terms, it's stating the property `a * 1 = a` for all `a` in a right cancelable monoid.
More concisely: In a right cancelable monoid, the right identity element (1) multiplied with any element `a` results in `a` itself (i.e., `a * 1 = a`).
|
AddMonoid.nsmul_succ
theorem AddMonoid.nsmul_succ :
∀ {M : Type u} [self : AddMonoid M] (n : ℕ) (x : M), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
This theorem states that for any type `M` which has an `AddMonoid` structure, and for any natural number `n` and element `x` in `M`, the operation of natural number multiplication (denoted as `AddMonoid.nsmul`) with `(n + 1)` and `x` is equivalent to the addition of `AddMonoid.nsmul` with `n` and `x`, and `x` itself. In other words, it says that "multiplying" an element by `(n + 1)` in the additive monoid is the same as "multiplying" it by `n` and then adding the element once more.
More concisely: For any `AddMonoid M`, `n : ℕ`, and `x : M`, `AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x`.
|
IsRightCancelAdd.add_right_cancel
theorem IsRightCancelAdd.add_right_cancel :
∀ {G : Type u} [inst : Add G] [self : IsRightCancelAdd G] (a b c : G), a + b = c + b → a = c
This theorem states that addition is right cancellative. In other words, for any type `G` that has an addition operation and the property `IsRightCancelAdd`, if we have three elements `a`, `b`, and `c` of type `G` such that `a + b` equals `c + b`, then `a` must be equal to `c`. This essentially says that if the sums of `a` and `b` and `c` and `b` are equal, `b` can be cancelled from both sides, leaving `a` equal to `c`.
More concisely: If `G` is a type with an addition operation and `IsRightCancelAdd` property, then for all `a`, `b`, and `c` in `G`, if `a + b = c + b`, then `a = c`.
|
AddLeftCancelMonoid.zero_add
theorem AddLeftCancelMonoid.zero_add : ∀ {M : Type u} [self : AddLeftCancelMonoid M] (a : M), 0 + a = a
This theorem states that zero is a left neutral element for the operation of addition in an AddLeftCancelMonoid. That is, for any object `a` in a type `M` that forms an AddLeftCancelMonoid, the sum of `0` and `a` equals `a`. The AddLeftCancelMonoid is a mathematical structure where addition is a binary operation and has a property that allows the cancellation of a common term from the left side of the equation.
More concisely: In an AddLeftCancelMonoid, the additive identity (0)Left distributes over every element `a`, i.e., 0 + a = a.
|
AddLeftCancelMonoid.nsmul_succ
theorem AddLeftCancelMonoid.nsmul_succ :
∀ {M : Type u} [self : AddLeftCancelMonoid M] (n : ℕ) (x : M),
AddLeftCancelMonoid.nsmul (n + 1) x = AddLeftCancelMonoid.nsmul n x + x
The theorem `AddLeftCancelMonoid.nsmul_succ` states that for any type `M` that has an `AddLeftCancelMonoid` structure, for any natural number `n` and any element `x` of `M`, the operation of multiplying (in the additive sense) `x` by `(n + 1)` is equivalent to multiplying `x` by `n` and then adding `x`. In other words, it asserts that the operation `nsmul` defined in the context of `AddLeftCancelMonoid` satisfies the natural peano axiom for multiplication: $(n + 1) \cdot x = n \cdot x + x$.
More concisely: For any AddLeftCancelMonoid `M` and natural number `n` and element `x` of `M`, `nsmul x (n + 1) = nsmul x n + x`.
|
MulOneClass.one_mul
theorem MulOneClass.one_mul : ∀ {M : Type u} [self : MulOneClass M] (a : M), 1 * a = a
This theorem, titled 'MulOneClass.one_mul', asserts that in any mathematical structure of type 'M' which is an instance of the 'MulOneClass' (which signifies structures with a multiplication operation and a distinct 'one' element), multiplying 'one' ('1') to the left of any element (denoted 'a') of this structure always yields the same element 'a'. In more formal terms, for all elements 'a' of type 'M', the equality 1 * a = a holds true.
More concisely: For all elements $a$ in any MulOneClass structure, we have $1 \cdot a = a$.
|
Monoid.npow_zero
theorem Monoid.npow_zero : ∀ {M : Type u} [self : Monoid M] (x : M), Monoid.npow 0 x = 1
This theorem states that for any type `M` that is a monoid, raising any element `x` of `M` to the power of zero (using the `Monoid.npow` function) results in the multiplicative identity of the monoid, denoted as `1`. This is in line with the general mathematical principle that any number raised to the power of zero is equal to one.
More concisely: For any monoid `M` and element `x` in `M`, `Monoid.npow x 0 = 1`.
|
zpow_zero
theorem zpow_zero : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a : G), a ^ 0 = 1
This theorem asserts that for any type `G` that forms a `DivInvMonoid`, raising any element `a` of `G` to the power of zero yields the identity element of the monoid. In mathematical terms, given a division-invertible monoid `G` and any element `a` in `G`, `a` to the power of 0 is 1, where 1 represents the identity element in the given monoid structure.
More concisely: For any division-invertible monoid `G` and its element `a`, `a^0 = 1`.
|
IsLeftCancelMul.mul_left_cancel
theorem IsLeftCancelMul.mul_left_cancel :
∀ {G : Type u} [inst : Mul G] [self : IsLeftCancelMul G] (a b c : G), a * b = a * c → b = c
The theorem `IsLeftCancelMul.mul_left_cancel` asserts that multiplication in a type `G` equipped with a multiplication operation is left cancellative. This means for any three elements `a`, `b`, and `c` in `G`, if the product of `a` and `b` equals the product of `a` and `c`, then `b` must be equal to `c`. In other words, if we multiply the same number on the left of two different numbers and the results are equal, then the two different numbers must be the same.
More concisely: If `a` is an element of a group `G` and `b`, `c` are any two elements such that `a * b = a * c`, then `b = c`.
|
neg_eq_of_add_eq_zero_left
theorem neg_eq_of_add_eq_zero_left : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, a + b = 0 → -b = a := by
sorry
This theorem states that for any type `G` which is an instance of a `SubtractionMonoid`, given two elements `a` and `b` of `G`, if the sum of `a` and `b` equals zero, then the additive inverse of `b` is equal to `a`. This is an algebraic property closely related to the definition of subtraction in a subtraction monoid. Essentially, it's saying that if adding `b` to `a` results in zero, then `a` must be the value that negates `b`, i.e., `-b = a`.
More concisely: If `G` is a subtraction monoid and `a`, `b` are its elements with `a + b = 0`, then `b` is the additive inverse of `a`, i.e., `a = -b`.
|
AddMonoid.zero_add
theorem AddMonoid.zero_add : ∀ {M : Type u} [self : AddMonoid M] (a : M), 0 + a = a
This theorem states that zero is a left neutral element for the addition operation in any AddMonoid. In other words, for any type `M` that has an AddMonoid structure (denoted by `[self : AddMonoid M]`), adding zero (`0`) to any element `a` of `M` (expressed as `0 + a`) always equals `a`. This property is a fundamental part of the definition of an additive monoid, which is a set equipped with an associative addition operation and a neutral element `0`.
More concisely: For any AddMonoid `M`, the additive identity `0` satisfies `0 + a = a` for all `a` in `M`.
|
mul_inv_cancel_left
theorem mul_inv_cancel_left : ∀ {G : Type u_1} [inst : Group G] (a b : G), a * (a⁻¹ * b) = b
This theorem states that for any given group `G`, and for any elements `a` and `b` from this group, the product of `a` and the result of the multiplication of the inverse of `a` (`a⁻¹`) with `b` is equal to `b`. In mathematical terms, we could express this as: for any `a`, `b` in a group `G`, `a * (a⁻¹ * b) = b`. This theorem is essentially about the 'cancellation' property in group theory, which allows one to simplify expressions by 'canceling out' terms.
More concisely: In any group, for all elements `a` and `b`, `a * (a⁻¹ * b) = b`.
|
mul_one
theorem mul_one : ∀ {M : Type u} [inst : MulOneClass M] (a : M), a * 1 = a
This theorem states that for any type `M` that has a multiplication operation and a specified element considered as 'one' (i.e., it belongs to the `MulOneClass`), multiplying any element `a` of type `M` by this 'one' will yield `a` itself. This is a formalization of the multiplicative identity property in mathematics, which states that any number multiplied by 1 remains unchanged.
More concisely: For any type `M` with multiplication and a multiplicative identity `one`, `a * one = a` for all `a : M`.
|
pow_succ
theorem pow_succ : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a ^ n * a
This theorem, named `pow_succ`, is a statement about the power operation in the context of a monoid. The theorem holds for any type `M` that has a `Monoid` structure. Given an element `a` of type `M` and an natural number `n`, the theorem states that raising `a` to the power of `n + 1` is equivalent to multiplying `a` raised to the power of `n` by `a`. This corresponds to the well-known property of exponentiation that `a` to the power of `n+1` is just `a` to the power of `n` times `a`.
More concisely: For any monoid `M` and element `a` in `M` and natural number `n`, `a^(n + 1)` equals `a^n * a`.
|
CommMagma.IsLeftCancelMul.toIsRightCancelMul
theorem CommMagma.IsLeftCancelMul.toIsRightCancelMul :
∀ (G : Type u) [inst : CommMagma G] [inst_1 : IsLeftCancelMul G], IsRightCancelMul G
This theorem states that for any type `G` that is a commutative magma (`CommMagma G`), if left cancellation law for multiplication holds (`IsLeftCancelMul G`), then the right cancellation law for multiplication also holds (`IsRightCancelMul G`). In other words, in this type `G`, if for all `a, b, c` in `G`, `a * b = a * c` implies `b = c`, then it is also the case that `b * a = c * a` implies `b = c`. Here the operation `*` is the binary operation defined in the commutative magma.
More concisely: In a commutative magma `G` where left cancellation law for multiplication holds, right cancellation law for multiplication also holds. That is, if `a * b = a * c` implies `b = c`, then also `b * a = c * a` implies `b = c`.
|
DivInvMonoid.div_eq_mul_inv
theorem DivInvMonoid.div_eq_mul_inv : ∀ {G : Type u} [self : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
This theorem states that in any division inversion monoid `G`, the division operation (`a / b`) is defined as the multiplication of `a` by the inverse of `b` (`a * b⁻¹`). A division inversion monoid is a specific type of algebraic structure that includes operations for multiplication, inverse, and an identity element.
More concisely: In a division inversion monoid, division is equivalent to multiplication with the inverse.
|
mul_left_inv
theorem mul_left_inv : ∀ {G : Type u_1} [inst : Group G] (a : G), a⁻¹ * a = 1
This theorem states that for any type `G` that is a group, for any element `a` of `G`, the product of the inverse of `a` and `a` itself equals the identity element of the group. This is a fundamental property of groups, expressing that multiplying any element by its inverse results in the group's identity element.
More concisely: For any group `G` and element `a` in `G`, `a`'s inverse multiplied by `a` equals the identity element of `G`. In Lean notation: `∀ (G : Type) [group G], ∃ (ha : is_group G), ∀ (a : G), inv a * a = id G`.
|
mul_right_cancel_iff
theorem mul_right_cancel_iff :
∀ {G : Type u_1} [inst : Mul G] [inst_1 : IsRightCancelMul G] {a b c : G}, b * a = c * a ↔ b = c
This theorem states that for any type `G` that has a multiplication operation and satisfies the right cancellation property (meaning for all `a`, `b`, `c` in `G`, `a * b = a * c` implies `b = c`), the equality `b * a = c * a` is equivalent to `b = c`. This is analogous to being able to "cancel out" the `a` on both sides of the equation in ordinary arithmetic.
More concisely: If `G` is a type with multiplication and right cancellation property, then `b * a = c * a` implies `b = c`.
|
mul_right_cancel
theorem mul_right_cancel :
∀ {G : Type u_1} [inst : Mul G] [inst_1 : IsRightCancelMul G] {a b c : G}, a * b = c * b → a = c
This theorem, `mul_right_cancel`, states that for any type `G` equipped with a multiplication operation and the property of right cancellation, and for any elements `a`, `b`, and `c` of type `G`, if the multiplication of `a` and `b` equals the multiplication of `c` and `b`, then `a` must be equal to `c`. In other words, it states that multiplication in such a setting is 'right cancellable': if `a * b = c * b`, we can 'cancel out' the `b` on the right side of both equations to get `a = c`. This property is crucial in structures like groups or fields where operations have certain cancellation properties.
More concisely: If `a * b = c * b` in a type `G` with right cancellation, then `a = c`.
|
Semigroup.mul_assoc
theorem Semigroup.mul_assoc : ∀ {G : Type u} [self : Semigroup G] (a b c : G), a * b * c = a * (b * c)
This theorem states that multiplication is associative in any semigroup. Given a semigroup of type `G`, for any three elements `a`, `b`, and `c` in this semigroup, the result of multiplying `a` and `b` together and then multiplying the result by `c` is the same as the result of multiplying `b` and `c` together first, then multiplying `a` by this result. In mathematical notation, this is expressed as `a * b * c = a * (b * c)`.
More concisely: In any semigroup, the order of multiplication of elements does not affect the result: `a * b * c = a * (b * c)`.
|
Monoid.npow_succ
theorem Monoid.npow_succ :
∀ {M : Type u} [self : Monoid M] (n : ℕ) (x : M), Monoid.npow (n + 1) x = Monoid.npow n x * x
The theorem `Monoid.npow_succ` states that for any type `M` that forms a monoid structure, and for any natural number `n` and element `x` of type `M`, the operation of raising `x` to the power of `(n + 1)` is equivalent to raising `x` to the power of `n` and then multiplying the result by `x`. This captures the intuitive behavior of exponentiation in the context of a monoid.
More concisely: For any monoid `M`, `n : ℕ`, and `x : M`, `x ^ (n + 1) = x ^ n * x`.
|
mul_inv_rev
theorem mul_inv_rev : ∀ {G : Type u_1} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
This theorem, named `mul_inv_rev`, states that for any type `G` that forms a Division Monoid, the multiplicative inverse of the product of two elements `a` and `b` in `G`, is equal to the product of the inverse of `b` and the inverse of `a`. In traditional mathematical notation, this theorem says that for any `a`, `b` in a Division Monoid `G`, (ab)⁻¹ = b⁻¹a⁻¹. This is the reverse order of multiplication of the inverses, hence the name `mul_inv_rev`.
More concisely: For any division monoid `G` and elements `a`, `b` in `G`, the multiplicative inverse of their product is equal to the product of their inverses in reverse order: (ab)⁻¹ = b⁻¹a⁻¹.
|
add_zero
theorem add_zero : ∀ {M : Type u} [inst : AddZeroClass M] (a : M), a + 0 = a
This theorem states that for any type `M` that has an addition operation and a zero element, the addition of any element `a` of type `M` with the zero element results in `a` itself. In terms of mathematics, it means for any algebraic structure with addition operation and zero (0), adding zero to any element does not change the value of the element. This is equivalent to the common concept in mathematics where `a + 0 = a` for any `a`.
More concisely: For any type `M` with an addition operation and a zero element, `a + 0 = a` for all `a` in `M`.
|
RightCancelMonoid.one_mul
theorem RightCancelMonoid.one_mul : ∀ {M : Type u} [self : RightCancelMonoid M] (a : M), 1 * a = a
This theorem states that for any type `M` that is a right cancelable monoid, one (`1`) acts as a left neutral element with respect to the multiplication operation. In other words, for any element `a` of `M`, the product of `1` and `a` equals `a`. In mathematical terms, this can be written as `1*a = a` for all `a` in `M`.
More concisely: For any right cancelable monoid `M`, the multiplicative identity `1` is its left neutral element, i.e., `1 * a = a` for all `a` in `M`.
|
eq_neg_of_add_eq_zero_left
theorem eq_neg_of_add_eq_zero_left : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, a + b = 0 → a = -b := by
sorry
This theorem states that for any type `G` that is a subtraction monoid, and any two elements `a` and `b` of this type, if the sum of `a` and `b` equals zero, then `a` is equal to the negation of `b`. This theorem thus represents the property of additive inverses in a subtraction monoid, a structure that has an operation akin to subtraction.
More concisely: If `G` is a subtraction monoid and `a`, `b` ∈ `G` satisfy `a + b = 0`, then `a = -b`.
|
mul_right_inv
theorem mul_right_inv : ∀ {G : Type u_1} [inst : Group G] (a : G), a * a⁻¹ = 1
This theorem states that for any type `G` that is a Group, the multiplication of any element `a` in `G` with its inverse `a⁻¹` results in the identity element `1`. This is a fundamental property of groups in mathematics, where each element has an inverse such that their multiplication equals the group's identity element.
More concisely: For all groups G and all elements a in G, a * a⁻₁ = 1.
|
Monoid.mul_one
theorem Monoid.mul_one : ∀ {M : Type u} [self : Monoid M] (a : M), a * 1 = a
This theorem states that one is a right neutral element for the multiplication operation in a monoid. In other words, for any type `M` that is a monoid, and for any element `a` of this type, multiplying `a` by `one` results in `a`. In mathematical notations, ∀ a ∈ M, a * 1 = a.
More concisely: For any monoid `M` and element `a` in `M`, `a * one(M) = a`.
|
CommMagma.mul_comm
theorem CommMagma.mul_comm : ∀ {G : Type u} [self : CommMagma G] (a b : G), a * b = b * a
The given theorem states that in a commutative multiplicative magma (a mathematical structure featuring a single associative binary operation that is commutative), the multiplication operation is commutative. This means that for any two elements `a` and `b` of type `G` (which is a commutative multiplicative magma), the result of `a * b` is equal to the result of `b * a`.
More concisely: In a commutative multiplicative magma, the multiplication operation is commutative, i.e., `a * b = b * a` for all `a` and `b` of type `G`.
|
neg_add_cancel_right
theorem neg_add_cancel_right : ∀ {G : Type u_1} [inst : AddGroup G] (a b : G), a + -b + b = a
This theorem, `neg_add_cancel_right`, states that for any type `G` that has an `AddGroup` structure (i.e., an additive group), for any two elements `a` and `b` from `G`, if we add the negation of `b` to `a` and then add `b`, we get `a` back. In mathematical terms, it states that for all `a` and `b` in the additive group `G`, the equation `a + -b + b = a` holds true. This is a basic property of additive groups, reflecting the fact that adding an element and its negation results in a neutral element of the group (usually denoted as zero), essentially canceling each other out.
More concisely: For any additive group `G` and elements `a` and `b` in `G`, `a + (-b) = a`.
|
AddCommMagma.IsRightCancelAdd.toIsCancelAdd
theorem AddCommMagma.IsRightCancelAdd.toIsCancelAdd :
∀ (G : Type u) [inst : AddCommMagma G] [inst_1 : IsRightCancelAdd G], IsCancelAdd G
This theorem states that for any type `G` equipped with the structure of an `AddCommMagma` (which is a set with a binary operation that is associative and commutative), if `G` has the property `IsRightCancelAdd` (which means that for all elements `a, b, c` in `G`, if `a + b = a + c`, then `b = c`), then `G` also has the property `IsCancelAdd` (which means that for all elements `a, b, c` in `G`, if `a + b = c + a`, then `b = c`). In other words, if addition on `G` is right-cancellable, then it is also cancellative.
More concisely: If a commutative additive magma `G` has the right cancellation property, then it has the cancellation property.
|
neg_add_rev
theorem neg_add_rev : ∀ {G : Type u_1} [inst : SubtractionMonoid G] (a b : G), -(a + b) = -b + -a
This theorem, `neg_add_rev`, states that for any type `G` that is a subtraction monoid, the additive inverse of the sum of two elements `a` and `b` (i.e., `-(a + b)`) is equal to the sum of the additive inverses of `b` and `a` (i.e., `-b + -a`). This is basically a restatement in a monoid context of the well-known property from elementary mathematics that the negation of a sum can be distributed over the summands.
More concisely: For any subtraction monoid `G`, the additive inverse of `a + b` equals `-a + -b`.
|
LeftCancelMonoid.npow_succ
theorem LeftCancelMonoid.npow_succ :
∀ {M : Type u} [self : LeftCancelMonoid M] (n : ℕ) (x : M),
LeftCancelMonoid.npow (n + 1) x = LeftCancelMonoid.npow n x * x
This theorem states that, for any left cancel monoid `M` and any element `x` of `M`, raising `x` to the power of `(n + 1 : ℕ)` is the same as multiplying the result of `x` raised to the power of `n` by `x`. In other words, the function `LeftCancelMonoid.npow` exhibits the usual property of exponentiation: `x^(n+1) = x^n * x`.
More concisely: For any left cancel monoid `M` and its element `x`, the exponentiation function `npow x (n + 1)` equals the product of `npow x n` and `x`.
|
mul_left_cancel_iff
theorem mul_left_cancel_iff :
∀ {G : Type u_1} [inst : Mul G] [inst_1 : IsLeftCancelMul G] {a b c : G}, a * b = a * c ↔ b = c
This theorem, `mul_left_cancel_iff`, is a universal proposition in the context of a type `G` equipped with a multiplication operation (`Mul G`) and the property of left-cancellability (`IsLeftCancelMul G`). It states that for any three elements `a`, `b`, and `c` in `G`, the equality `a * b = a * c` is equivalent to `b = c`. In other words, if two products with the same left factor are equal, then the right factors must also be equal. This is essentially the cancellation law for multiplication on the left.
More concisely: If for all elements `a`, `b`, `c` in a group `G` with multiplication `Mul G` and left-cancellation property `IsLeftCancelMul G`, the equality `a * b = a * c` implies `b = c`.
|
mul_inv_cancel_right
theorem mul_inv_cancel_right : ∀ {G : Type u_1} [inst : Group G] (a b : G), a * b * b⁻¹ = a
This theorem, `mul_inv_cancel_right`, states that for any type `G` that forms a group, for any elements `a` and `b` of the group, the product of `a` and `b` multiplied by the inverse of `b`, or `b⁻¹`, is equal to `a`. Essentially, it expresses the property of a group where the product of an element and its inverse cancels out on the right side, leaving the other factor unchanged.
More concisely: For any group `G` and elements `a, b` in `G`, `a * b ^-1 = a`.
|
zpow_negSucc
theorem zpow_negSucc : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a : G) (n : ℕ), a ^ Int.negSucc n = (a ^ (n + 1))⁻¹
This theorem states that for any type `G` that forms a `DivInvMonoid` (a structure with division and inversion operations), and any element `a` of type `G` and a natural number `n`, raising `a` to the power of the negation of the successor of `n` (in terms of integers, represented by `Int.negSucc n`) is equivalent to taking the inverse (`⁻¹`) of `a` raised to the power of `n+1`. In mathematical notation, this would be written as `a ^ - (n + 1) = 1 / (a ^ (n + 1))`.
More concisely: For any `DivInvMonoid` type `G` and its element `a` and natural number `n`, `a ^ (negation (succ n)) = 1 / (a ^ (n + 1))`.
|