one_div_div
theorem one_div_div : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b : α), 1 / (a / b) = b / a
This theorem, named `one_div_div`, states that for any type `α` that forms a Division Monoid, given any two elements `a` and `b` of type `α`, the expression `1 / (a / b)` is equal to `b / a`. In simple mathematical terms, it states that one divided by the result of `a` divided by `b` is equal to `b` divided by `a`. This theorem holds true for all division monoids, which are algebraic structures with an operation mimicking division.
More concisely: For any division monoid `α`, the expressions `1 / (a / b)` and `b / a` are equal for all `a` and `b` in `α`.
|
sub_eq_zero_of_eq
theorem sub_eq_zero_of_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a = b → a - b = 0
This theorem, `sub_eq_zero_of_eq`, is essentially an alias of the reverse direction of another theorem named `sub_eq_zero`. The theorem states that for any AddGroup `G` and any two element `a` and `b` of the same type, if `a` equals `b`, then the subtraction of `b` from `a` equals zero. The `AddGroup` is a mathematical structure in group theory where addition is the group operation.
More concisely: If `a` and `b` are elements of an AddGroup, then `a - b = 0` if and only if `a = b`.
|
Mathlib.Algebra.Group.Basic._auxLemma.19
theorem Mathlib.Algebra.Group.Basic._auxLemma.19 :
∀ {α : Type u_1} [inst : DivisionMonoid α] {a : α}, (a⁻¹ = 1) = (a = 1)
This theorem, `Mathlib.Algebra.Group.Basic._auxLemma.19`, states that for any type `α` equipped with a division operation, denoted as a division monoid, for any element `a` of that type, `a` being equal to `1` is equivalent to the inverse of `a` being `1`. In mathematical notation, this could be written as: for all `a` in `α`, `a⁻¹ = 1` if and only if `a = 1`.
More concisely: For any division monoid `α`, the element `a` has an inverse equal to `1` if and only if `a` is the identity element `1` itself.
|
sub_add_eq_sub_sub
theorem sub_add_eq_sub_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - (b + c) = a - b - c
This theorem, `sub_add_eq_sub_sub`, states that for any type `α` that is a subtraction commutative monoid (i.e., a mathematical structure equipped with addition, subtraction and zero, where subtraction is commutative), and for any three elements `a`, `b`, and `c` of that type, the subtraction of the sum of `b` and `c` from `a` is equal to the result of subtracting `c` from the difference of `a` and `b`. In mathematical notation, it expresses the relation: `a - (b + c) = a - b - c`.
More concisely: For any subtraction commutative monoid type `α` and elements `a`, `b`, `c` of `α`, `a - (b + c) = a - b - c`.
|
sub_eq_self
theorem sub_eq_self : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a - b = a ↔ b = 0
This theorem states that for all types `G` that have an additive group structure, the difference of two elements `a` and `b` of `G` is equal to `a` if and only if `b` is the zero element of the group. In mathematical terms, it states that for all `a` and `b` in an additive group `G`, `a - b = a` if and only if `b = 0`.
More concisely: For every additive group `G`, the element `b` is the zero element of `G` if and only if the difference of any element `a` from `G` and `b` is equal to `a`.
|
neg_add
theorem neg_add : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -(a + b) = -a + -b
This theorem, named `neg_add`, states that for any type `α` that forms a subtraction commutative monoid, the negation of the sum of any two elements `a` and `b` of that type is equal to the sum of the negation of `a` and the negation of `b`. In mathematical notation, this would be `-(a + b) = -a + -b` for all `a` and `b` in `α`.
More concisely: For any commutative monoid `α` with negation operation, `-`, it holds that `-(a + b) = -a + -b` for all `a, b` in `α`.
|
div_mul_div_cancel'
theorem div_mul_div_cancel' : ∀ {G : Type u_3} [inst : Group G] (a b c : G), a / b * (b / c) = a / c
This theorem states that for any group `G` and any elements `a`, `b`, and `c` of `G`, the result of dividing `a` by `b`, and then multiplying that by the result of dividing `b` by `c`, is equal to the result of dividing `a` by `c`. This can be thought of as a type of "cancellation" rule for division and multiplication in groups. The theorem holds for any group, under the assumption that the group operation behaves as division does in the field of real numbers.
More concisely: For any group `G` and elements `a`, `b`, and `c` in `G`, `(a / b) * (b / c) = a / c`.
|
sub_sub
theorem sub_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - b - c = a - (b + c)
This theorem states that for all instances of a type `α` in a subtraction commutative monoid, the subtraction of `b` and `c` from `a` in sequence (i.e., `(a - b) - c`) is the same as subtracting the sum of `b` and `c` from `a` once (i.e., `a - (b + c)`). This is a property of subtraction in the context of commutative monoids.
More concisely: For all commutative monoids `α`, and all elements `a`, `b`, and `c` of `α`, `(a - b) - c = a - (b + c)`.
|
inv_div
theorem inv_div : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b : α), (a / b)⁻¹ = b / a
This theorem, called `inv_div`, states that for all `a` and `b` in a Division Monoid `α`, the inverse of the division of `a` by `b` is equal to the division of `b` by `a`. In mathematical notation, this means that for all `a, b` in a given group equipped with an operation of division, `(a / b)⁻¹ = b / a`. This is a fundamental property in the field of algebra where the Division Monoid is a structure consisting of a set equipped with an associative binary operation and an invertible element.
More concisely: For all `a, b` in a Division Monoid `α`, `(a / b)⁻¹ = b / a`.
|
Mathlib.Algebra.Group.Basic._auxLemma.22
theorem Mathlib.Algebra.Group.Basic._auxLemma.22 :
∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, (0 = -a) = (a = 0)
This theorem, named `Mathlib.Algebra.Group.Basic._auxLemma.22`, states that for any type `α` equipped with a `SubtractionMonoid` structure and for any element `a` of that type, the statement that `0` equals the negation of `a` (`0 = -a`) is equivalent to the statement that `a` equals `0` (`a = 0`). Essentially, in the context of a subtraction monoid, an element being its own additive inverse implies that this element is the additive identity `0`.
More concisely: In a subtraction monoid, an element is the additive identity if and only if it is its own additive inverse.
|
Mathlib.Algebra.Group.Basic._auxLemma.8
theorem Mathlib.Algebra.Group.Basic._auxLemma.8 :
∀ {M : Type u} [inst : AddLeftCancelMonoid M] {a b : M}, (a = a + b) = (b = 0)
This theorem, `Mathlib.Algebra.Group.Basic._auxLemma.8`, states that for any type `M` that forms an additive left-cancellable monoid, for any two elements `a` and `b` in the monoid, `a` is equal to `a + b` if and only if `b` is the zero element of the monoid. This is because in an additive left-cancellable monoid, the cancellation law allows any term that appears on both sides of an equation to be subtracted out.
More concisely: In an additive left-cancellative monoid, for all elements `a` and `b`, `a = a + b` if and only if `b` is the additive identity.
|
sub_sub_sub_cancel_right
theorem sub_sub_sub_cancel_right : ∀ {G : Type u_3} [inst : AddGroup G] (a b c : G), a - c - (b - c) = a - b
This theorem states that for all types `G` that form an additive group, for any three elements `a`, `b`, and `c` in this group, the expression `a - c - (b - c)` simplifies to `a - b`. In mathematical notation, for all $a, b, c \in G$, where $G$ is an additive group, we have that $a - c - (b - c) = a - b$.
More concisely: For all additive groups G and elements a, b, c in G, the expression a - c - (b - c) equals a - b.
|
neg_involutive
theorem neg_involutive : ∀ {G : Type u_3} [inst : InvolutiveNeg G], Function.Involutive Neg.neg
This theorem states that for any type `G` that has the property `InvolutiveNeg` (which usually means that negation operation on elements of `G` is involutive), the negation function `Neg.neg` is an involutive function. In other words, applying the negation function twice on any element from `G` will return the original element. This corresponds to the mathematical property that the negative of the negative of a number is the number itself, i.e., `−(−a) = a` for any number `a` in `G`.
More concisely: For any type `G` with involutive negation, negation is an involutive function, i.e., `Neg.neg (x : G) = x`.
|
inv_mul_eq_one
theorem inv_mul_eq_one : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a⁻¹ * b = 1 ↔ a = b
This theorem states that for any type `G` that forms a group, given any two elements `a` and `b` of the group, the product of the inverse of `a` and `b` equals the identity element (denoted by `1` in algebraic structures) if and only if `a` equals `b`. In other words, in a group, a number multiplied by its inverse results in the identity element.
More concisely: In a group, for all elements `a` and `b`, `a * a⁻¹ = b * b⁻¹` if and only if `a = b`, where `*` denotes group multiplication and `⁻¹` denotes the inverse.
|
eq_div_iff_mul_eq'
theorem eq_div_iff_mul_eq' : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a = b / c ↔ a * c = b
This theorem states that for any type `G` that forms a group, and for any elements `a`, `b`, and `c` of that group, `a` is equal to `b` divided by `c` if and only if `a` multiplied by `c` is equal to `b`. This provides a connection between division and multiplication in a group, allowing one to transition between these two operations under certain conditions.
More concisely: For any group `G` and elements `a`, `b`, and `c` in `G`, `a = b / c` if and only if `a * c = b`.
|
div_eq_inv_mul
theorem div_eq_inv_mul : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), a / b = b⁻¹ * a
This theorem states that for any division commutative monoid `α` and any elements `a` and `b` of `α`, the operation of dividing `a` by `b` is equivalent to multiplying the inverse of `b` by `a`. In mathematical terms, it expresses that `a / b = b⁻¹ * a` for all `a` and `b` in the division commutative monoid `α`.
More concisely: For any division commutative monoid `α`, the operation of dividing `a` by `b` is equivalent to multiplying the inverse of `b` by `a`, that is, `a / b ≈ b⁻¹ * a`.
|
sub_self
theorem sub_self : ∀ {G : Type u_3} [inst : AddGroup G] (a : G), a - a = 0
This theorem, `sub_self`, states that for all types `G` that have an `AddGroup` structure, the subtraction of any element `a` from itself results in the identity element of addition, which is `0`. In other words, in any additive group, subtracting any element from itself always yields `0`.
More concisely: For any type `G` with an `AddGroup` structure, `a` being an element of `G`, we have `a - a = 0`.
|
neg_inj
theorem neg_inj : ∀ {G : Type u_3} [inst : InvolutiveNeg G] {a b : G}, -a = -b ↔ a = b
This theorem, `neg_inj`, states that for any type `G` with an involutive negation operation, the negation of `a` is equal to the negation of `b` if and only if `a` is equal to `b`. In other words, negation is an injective (one-to-one) function in this context.
More concisely: For any type `G` equipped with an involutive negation operation, negation is a function that maps distinct elements to distinct negated elements.
|
mul_div_cancel''
theorem mul_div_cancel'' : ∀ {G : Type u_3} [inst : Group G] (a b : G), a * b / b = a
This theorem, referred to as an alias of `mul_div_cancel_right`, deals with the concepts of multiplication and division in the area of group theory. In the context of any group `G`, for any elements `a` and `b` of `G`, the theorem states that if you multiply `a` and `b` together and then divide the result by `b`, you get back `a`. This reflects the property of groups where division undoes multiplication.
More concisely: In any group, for all elements a and b, a * b / b = a.
|
add_left_inj
theorem add_left_inj :
∀ {G : Type u_3} [inst : Add G] [inst_1 : IsRightCancelAdd G] (a : G) {b c : G}, b + a = c + a ↔ b = c
This theorem states that, for any type `G` which is equipped with addition and has the right-cancellation property, if the addition of any element `a` with another element `b` equals to the addition of `a` with a third element `c`, then `b` is equal to `c`. In other words, if `b + a = c + a` then `b = c`. The right-cancellation property ensures that if you add the same quantity to two equal quantities, the results are still equal, which allows us to "cancel" `a` from both sides of the equation.
More concisely: For type `G` with addition and right cancellation property, if `a + b = a + c`, then `b = c`.
|
mul_eq_one_iff_eq_inv
theorem mul_eq_one_iff_eq_inv : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a * b = 1 ↔ a = b⁻¹
This theorem states that for any type `G` that has a group structure, and for any elements `a` and `b` of this type, the product `a * b` equals the identity element `1` if and only if `a` equals the inverse of `b`, denoted by `b⁻¹`. In other words, in a group, the only way the product of two elements can be the identity is if one is the inverse of the other.
More concisely: In a group, for all elements `a` and `b`, `a * b = 1` if and only if `a = b⁻¹`.
|
mul_left_inj
theorem mul_left_inj :
∀ {G : Type u_3} [inst : Mul G] [inst_1 : IsRightCancelMul G] (a : G) {b c : G}, b * a = c * a ↔ b = c
This theorem, `mul_left_inj`, states that for any type `G` that has a multiplication operation (`Mul G`) and satisfies the right cancellation law for multiplication (`IsRightCancelMul G`), for any element `a` of type `G`, `b` and `c` are equal if and only if the product of `b` and `a` is equal to the product of `c` and `a`. Essentially, this theorem gives us a rule for canceling the same factor from both sides of an equation in this mathematical structure. This corresponds to the intuitive idea of "cancellation" from elementary algebra.
More concisely: For any type `G` with multiplication `Mul G` and right cancellation law `IsRightCancelMul G`, the equation `b * a = c * a` implies `b = c`.
|
eq_neg_iff_add_eq_zero
theorem eq_neg_iff_add_eq_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a = -b ↔ a + b = 0
This theorem, `eq_neg_iff_add_eq_zero`, states that for any type `G` that is an additive group, and for any two elements `a` and `b` from `G`, `a` is equal to the negation of `b` if and only if the sum of `a` and `b` is zero. In mathematical terms, it's saying that for all a, b in an additive group G, a = -b if and only if a + b = 0.
More concisely: For any additive group G and elements a, b in G, a = -b if and only if a + b = 0.
|
Mathlib.Algebra.Group.Basic._auxLemma.31
theorem Mathlib.Algebra.Group.Basic._auxLemma.31 :
∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, (b - a = c - a) = (b = c)
This theorem, named `Mathlib.Algebra.Group.Basic._auxLemma.31`, declares that for any type `G` that forms an additive group, if the difference between values `b` and `a` is equal to the difference between values `c` and `a`, then `b` is equal to `c`. In mathematical terms, this can be expressed as: for all `a, b, c` in an additive group `G`, if `b - a = c - a`, then `b = c`.
More concisely: In an additive group, if the difference between two elements is equal to the difference between a third element and that same element, then the first two elements are equal.
|
sub_add_eq_add_sub
theorem sub_add_eq_add_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - b + c = a + c - b := by
sorry
This theorem states that for any type `α` that forms a subtraction commutative monoid, for any three elements `a`, `b`, and `c` of type `α`, the result of subtracting `b` from `a`, then adding `c` is equal to the result of adding `c` to `a`, then subtracting `b`. In mathematical notation, this would be written as: `a - b + c = a + c - b`.
More concisely: For any commutative subtraction monoid type `α`, the result of `a - b + c` is equal to `a + c - b`.
|
mul_inv_eq_iff_eq_mul
theorem mul_inv_eq_iff_eq_mul : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a * b⁻¹ = c ↔ a = c * b
This theorem states that for any type `G` that forms a Group, given any three elements `a`, `b`, and `c` of the group, the equality `a * b⁻¹ = c` is equivalent to `a = c * b`. Here, `*` denotes the group multiplication operation and `b⁻¹` is the inverse of `b` in the group. In other words, multiplying `a` by the inverse of `b` gives `c` if and only if `a` equals `c` multiplied by `b`.
More concisely: For any group `G` and elements `a, b, c` in `G`, `a * b⁻¹ = c` if and only if `a = c * b`.
|
mul_div_mul_right_eq_div
theorem mul_div_mul_right_eq_div : ∀ {G : Type u_3} [inst : Group G] (a b c : G), a * c / (b * c) = a / b
This theorem is stating that for any group `G`, and any elements `a`, `b`, and `c` of that group, the result of taking `a` times `c`, and then dividing it by the result of `b` times `c`, is equivalent to simply dividing `a` by `b`. In mathematical notation, this can be written as: \( \frac{a \cdot c}{b \cdot c} = \frac{a}{b} \). This equality holds true because of the properties of groups and their operation.
More concisely: For any group operation `*` and elements `a`, `b`, and `c` in the group, `(a * c) / (b * c) = a / b`.
|
inv_involutive
theorem inv_involutive : ∀ {G : Type u_3} [inst : InvolutiveInv G], Function.Involutive Inv.inv
This theorem states that for any type `G` that has the structure of `InvolutiveInv`, the operation `Inv.inv`, which inverts elements of `G`, is an involutive function. In other words, applying `Inv.inv` twice to any element of `G` will give back the original element. In the language of mathematics, if `Inv.inv` is denoted as `f`, then for all `x` in `G`, `f(f(x)) = x`.
More concisely: For any type `G` with an `InvolutiveInv` structure, the involution function `Inv.inv` is an involution, that is, `Inv.inv (Inv.inv x) = x` for all `x` in `G`.
|
mul_one_div
theorem mul_one_div : ∀ {G : Type u_3} [inst : DivInvMonoid G] (x y : G), x * (1 / y) = x / y
This theorem states that for any type `G` that has a `DivInvMonoid` instance (a type with division and inversion operations that obey certain laws), for any two elements `x` and `y` of this type, the result of multiplying `x` by the reciprocal of `y` (denoted as `1 / y`) is equal to the division of `x` by `y` (denoted as `x / y`).
More concisely: For any type `G` with a `DivInvMonoid` instance, `x / y = x * (1 / y)`.
|
neg_eq_zero
theorem neg_eq_zero : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, -a = 0 ↔ a = 0
This theorem, `neg_eq_zero`, states that for any type `α` that forms a subtraction monoid, the negation (in the context of the subtraction operation) of a variable `a` of type `α` equals zero if and only if `a` itself equals zero. A subtraction monoid is a structure with an associative operation (subtraction) and a special element (zero), and where every element has an additive inverse (which is obtained via subtraction from the zero element). Essentially, the theorem is saying that if you have an element from a set that behaves like numbers with respect to subtraction (e.g., the integers, real numbers, complex numbers etc.), then the only way for the negation of that element to be zero is if the element itself is zero.
More concisely: For any type `α` forming a subtraction monoid, `a` of type `α` has negation equal to zero if and only if `a` itself equals zero.
|
mul_div_mul_comm
theorem mul_div_mul_comm :
∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c d : α), a * b / (c * d) = a / c * (b / d)
This theorem, named `mul_div_mul_comm`, states that for any type `α` which is a Division Commutative Monoid, for any four elements `a`, `b`, `c`, and `d` of this type, the result of multiplying `a` and `b` and then dividing by the product of `c` and `d` is equal to the result of dividing `a` by `c` and multiplying by `b` divided by `d`. In other words, the equation $a * b / (c * d) = a / c * (b / d)$ holds true for any `a`, `b`, `c`, and `d` in any Division Commutative Monoid `α`.
More concisely: For any division commutative monoid `α`, the expression `a * b / (c * d)` equals `(a / c) * (b / d)` for all `a`, `b`, `c`, and `d` in `α`.
|
inv_surjective
theorem inv_surjective : ∀ {G : Type u_3} [inst : InvolutiveInv G], Function.Surjective Inv.inv
The theorem `inv_surjective` states that for all types `G` that have an involutive inverse structure (denoted `[inst : InvolutiveInv G]`), the inversion function (defined as `Inv.inv`) is surjective. In other words, for every element `g` in `G`, there exists some element `h` in `G` such that when `h` is inverted, it equals `g`. This is a fundamental property in the study of algebraic structures with inversion.
More concisely: For every type `G` equipped with an involutive inverse structure, the inversion function is a surjection.
|
add_sub_cancel'
theorem add_sub_cancel' : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a + b - a = b
This theorem, `add_sub_cancel'`, is an alias of `add_sub_cancel_left`. It states that for any type `G` that forms an additive commutative group, for any two elements `a` and `b` of this type, adding `a` and `b` and then subtracting `a` is equal to `b`. In other words, the operation of adding an element to another, and then subtracting the first element, effectively cancels out the first element, resulting in the second element. This can be written in mathematical notation as: ∀ a, b ∈ G, a + b - a = b, where G is an additive commutative group.
More concisely: For any additive commutative group G and elements a, b in G, a + b - a = b.
|
pow_ite
theorem pow_ite :
∀ {α : Type u_4} {β : Type u_5} [inst : Pow α β] (p : Prop) [inst_1 : Decidable p] (a : α) (b c : β),
(a ^ if p then b else c) = if p then a ^ b else a ^ c
This theorem states that for any types `α` and `β` where `α` has a power operation and a proposition `p` which is decidable, and any elements `a` of type `α` and `b, c` of type `β`, the power of `a` to the `b` if `p` is true or `c` if `p` is false is the same as `a` to the power of `b` if `p` is true or `a` to the power of `c` if `p` is false. In other words, it tells us that the exponentiation operation commutes with the if-then-else decision-making construct.
More concisely: For any types `α` with power operation, and decidable proposition `p`, and elements `a : α`, `b, c : β`, `a^(if p then b else c)` is equal to `(if p then a^b else a^c)`.
|
neg_add_eq_zero
theorem neg_add_eq_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, -a + b = 0 ↔ a = b
This theorem, `neg_add_eq_zero`, states that for all types `G` that have an additive group structure (`AddGroup G`), given any two elements `a` and `b` of `G`, the negation of `a` added to `b` equals zero if and only if `a` itself equals `b`. In mathematical notation, this can be expressed as $-a + b = 0 \Leftrightarrow a = b$, valid for all `a` and `b` belonging to the additive group `G`.
More concisely: For all additive groups `G`, `a`, and `b` in `G`, `-a + b = 0` if and only if `a = b`.
|
Mathlib.Algebra.Group.Basic._auxLemma.4
theorem Mathlib.Algebra.Group.Basic._auxLemma.4 :
∀ {G : Type u_3} [inst : Add G] [inst_1 : IsRightCancelAdd G] (a : G) {b c : G}, (b + a = c + a) = (b = c) := by
sorry
This theorem, `Mathlib.Algebra.Group.Basic._auxLemma.4`, states that for any type `G` that has an addition operation and the right cancellation property, given any elements `a`, `b`, `c` of `G`, if `b` added to `a` equals `c` added to `a`, then `b` equals `c`. In mathematical terms, this theorem asserts the right cancellation law of addition: if $b + a = c + a$, then $b = c$. This property is a fundamental one in the study of algebraic structures such as groups and rings.
More concisely: If `a` is an element of a type `G` with right cancellation property for addition, then `b = c` if and only if `b + a = c + a`.
|
div_eq_one_of_eq
theorem div_eq_one_of_eq : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a = b → a / b = 1
This theorem, "div_eq_one_of_eq", states that for any given type 'G' that is a Group, if two elements 'a' and 'b' of that group are equal, then the division of 'a' by 'b' equals 1. This is an alias of the reverse direction of another theorem named `div_eq_one`.
More concisely: If two elements in a group are equal, then their inverses are each other and their quotient is the identity element. (This is the statement for the reverse direction of the theorem `div_eq_one` in Lean 4, renamed as `div_eq_one_of_eq`.)
|
bit0_add
theorem bit0_add : ∀ {M : Type u} [inst : AddCommSemigroup M] (a b : M), bit0 (a + b) = bit0 a + bit0 b
This theorem, named "bit0_add", is a statement about addition in an additive commutative semigroup. Specifically, it says that for every type `M` equipped with an addition operation that forms a commutative semigroup, and for every two elements `a` and `b` of `M`, the operation of doubling (`bit0`) the sum of `a` and `b` is the same as the sum of the doubles of `a` and `b`. In mathematical terms, it is saying that for any `a` and `b` in `M`, 2*(a + b) = 2*a + 2*b, where '*' represents the operation of multiplication by 2 (or "doubling"), '+' is the addition operation in `M`, and '2' represents the double operation.
More concisely: For every commutative semigroup `M` with addition `+` and multiplication `*` by 2 (bit0), it holds that 2*(a + b) = 2*a + 2*b for all `a, b` in `M`.
|
div_eq_iff_eq_mul'
theorem div_eq_iff_eq_mul' : ∀ {G : Type u_3} [inst : CommGroup G] {a b c : G}, a / b = c ↔ a = b * c
This theorem, `div_eq_iff_eq_mul'`, states that for any type `G` that forms a Commutative Group, and for any elements `a`, `b`, and `c` of this type, the quotient of `a` divided by `b` being equal to `c` is logically equivalent to `a` being equal to the product of `b` and `c`. In mathematical terms, it's saying that $a / b = c$ if and only if $a = b * c$ in the context of a Commutative Group.
More concisely: In a commutative group, for all elements a, b, and c, a / b = c if and only if a = b * c.
|
sub_right_comm
theorem sub_right_comm : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - b - c = a - c - b := by
sorry
This theorem, `sub_right_comm`, states for any type `α` that is a commutative monoid under subtraction (that is, subtraction operation is associative and has an identity element, and it's commutative), the order of subtraction for any three elements `a`, `b`, and `c` of the type `α` does not matter when subtracting from the same element `a`. In mathematical terms, this theorem says that for any elements `a`, `b`, and `c` in a subtraction commutative monoid, `a - b - c` is equal to `a - c - b`.
More concisely: For any commutative monoid `α` under subtraction, the order of subtraction of elements `a, b, c` from `a` is commutative, that is, `a - b - c = a - c - b`.
|
mul_comm_div
theorem mul_comm_div : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a / b * c = a * (c / b)
This theorem states that for all types `α` that are instances of the division commutative monoid, and for any three elements `a`, `b`, and `c` of the type `α`, the operation of dividing `a` by `b` and then multiplying the result by `c` is equal to the operation of multiplying `a` by the result of dividing `c` by `b`. In mathematical terms, it is expressing the property that $\frac{a}{b} \cdot c = a \cdot \frac{c}{b}$ for all `a`, `b`, `c` in the division commutative monoid.
More concisely: For all division commutative monoids `α` and elements `a`, `b`, `c` in `α`, we have `(a / b) * c = a * (c / b)`.
|
eq_of_sub_eq_zero
theorem eq_of_sub_eq_zero : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, a - b = 0 → a = b
This theorem, `eq_of_sub_eq_zero`, states that for any type `α` that is a subtraction monoid (a set equipped with an operation, here subtraction, that is associative and has an identity element, typically zero), if the difference of two elements `a` and `b` of this type is zero (i.e., `a - b = 0`), then `a` and `b` are equal. In mathematical terms, for all `a` and `b` in some subtraction monoid, if `a - b` equals zero, then `a` equals `b`.
More concisely: If `α` is a subtraction monoid and `a - b = 0`, then `a = b`.
|
mul_div_assoc'
theorem mul_div_assoc' : ∀ {G : Type u_3} [inst : DivInvMonoid G] (a b c : G), a * (b / c) = a * b / c
This theorem states that for any type `G` that has a division and inverse operation (making it a `DivInvMonoid`), for all elements `a`, `b`, and `c` of `G`, the multiplication of `a` by the division of `b` by `c` is equal to the division of the multiplication of `a` and `b` by `c`. In mathematical notation, it says that $a \cdot \frac{b}{c} = \frac{a \cdot b}{c}$.
More concisely: For any `DivInvMonoid` type `G` and its elements `a`, `b`, and `c`, $a \cdot (b \div c) = (a \cdot b) \div c$.
|
sub_sub_sub_cancel_left
theorem sub_sub_sub_cancel_left : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), c - a - (c - b) = b - a := by
sorry
The theorem `sub_sub_sub_cancel_left` states that for any type `G` that forms an additive commutative group, for any elements `a`, `b`, `c` in `G`, the result of the operation `c - a - (c - b)` equals to `b - a`. This can be interpreted in terms of subtraction as: subtracting `a` from `c`, and then subtracting the result from `c - b` yields the same result as simply subtracting `a` from `b`.
More concisely: For any additive commutative group (G, +), and elements a, b, c in G, we have c - a - (c - b) = b - a.
|
multiplicative_of_isTotal
theorem multiplicative_of_isTotal :
∀ {α : Type u_1} {β : Type u_2} [inst : Monoid β] (r : α → α → Prop) [inst_1 : IsTotal α r] (f : α → α → β)
(p : α → Prop),
(∀ {a b : α}, p a → p b → f a b * f b a = 1) →
(∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c) →
∀ {a b c : α}, p a → p b → p c → f a c = f a b * f b c
The theorem states that for a binary function `f` from a type `α` equipped with a total relation `r` to a monoid `β`, if `f` is anti-symmetric (meaning that for any two elements `a` and `b` that satisfy a predicate `p`, `f a b * f b a = 1` holds), we can assert that `f` is multiplicative (meaning that for any three elements `a`, `b`, and `c` that satisfy the predicate `p`, `f a c = f a b * f b c` holds) by assuming `r a b` and `r b c` are satisfied. Here, "total relation" refers to a relation that holds for all pairs of elements in the set, and "monoid" refers to a set equipped with an associative binary operation and an identity element.
More concisely: Given a binary function `f` from a type `α` with total relation `r` to a monoid `β`, if `f` is anti-symmetric and `r` is satisfied for all pairs of elements, then `f` is multiplicative.
|
one_div
theorem one_div : ∀ {G : Type u_3} [inst : DivInvMonoid G] (a : G), 1 / a = a⁻¹
This theorem states that for any type `G` that is a Division Inverse Monoid (i.e., a set equipped with an operation, often multiplication, and an inversion operation that satisfies certain axioms), the operation of dividing 1 by any element `a` of `G` is equivalent to taking the inverse of `a`. In mathematical terms, we can express this as: ∀a ∈ G, 1/a = a⁻¹.
More concisely: For any Division Inverse Monoid `G`, the operation of taking inverses and dividing by an element `a` in `G` are equal, i.e., `a⁻¹ = 1/a`.
|
neg_injective
theorem neg_injective : ∀ {G : Type u_3} [inst : InvolutiveNeg G], Function.Injective Neg.neg
The theorem `neg_injective` states that for any type `G` that has the property of `InvolutiveNeg`, the minus or negation function (`Neg.neg`) is injective. In other words, if applying the negation function to two elements of `G` results in the same value, it implies that those two elements were originally the same. This is equivalent to saying that the negation function has the property that it never maps different elements to the same element.
More concisely: For any type `G` with the `InvolutiveNeg` property, the negation function `Neg.neg` is a bijection (i.e., both injective and surjective). Specifically, it is injective as stated in the theorem.
|
inv_eq_iff_eq_inv
theorem inv_eq_iff_eq_inv : ∀ {G : Type u_3} [inst : InvolutiveInv G] {a b : G}, a⁻¹ = b ↔ a = b⁻¹
This theorem states that for any type `G` that has an involutive inverse (involutive in this context means applying the operation twice yields the original element), and for any two elements `a` and `b` of `G`, the inverse of `a` is equal to `b` if and only if `a` is equal to the inverse of `b`. The `InvolutiveInv G` constraint ensures that `G` has an operation that can be applied twice to get back the original element, such as negation in the integers or complex conjugation in the complex numbers. This theorem essentially captures the symmetry in the action of the inversion operation.
More concisely: For any type `G` with an involutive operation and elements `a` and `b`, `a` and `b` have inverses of each other if and only if `a` is the inverse of `b` and `b` is the inverse of `a`.
|
div_div
theorem div_div : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a / b / c = a / (b * c)
This theorem, `div_div`, states that for any type `α` that has a structure of a commutative division monoid, for any three elements `a`, `b`, and `c` of this type, dividing `a` by `b`, and then the result by `c`, is equivalent to dividing `a` directly by the product of `b` and `c`. In mathematical notation, this would be expressed as $\frac{\frac{a}{b}}{c} = \frac{a}{b \cdot c}$.
More concisely: For any commutative division monoid type `α`, the quotient of `a` divided by `b` and then divided by `c` equals the quotient of `a` divided by the product of `b` and `c`. In Lean 4, this is expressed as the theorem `div_div : (∀ (α : Type) [CommMonoid α], ∀ (a b c : α), (a / b) / c = a / (b * c))`.
|
div_self'
theorem div_self' : ∀ {G : Type u_3} [inst : Group G] (a : G), a / a = 1
This theorem states that for any given type `G` that has a group structure, the division of any element `a` of `G` by itself always equals the group's identity element `1`. This is a generalization of the usual mathematical rule that any number divided by itself equals 1, extended to any group structure.
More concisely: For any group `G` and its element `a`, `a * inverse a = 1` holds.
|
neg_add_eq_sub
theorem neg_add_eq_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -a + b = b - a
This theorem states that for any type `α` that has a `SubtractionCommMonoid` instance (that is, a structure where subtraction is a commutative operation), for any two members `a` and `b` of type `α`, the negation of `a` added to `b` is equal to `b` subtracted by `a`. In mathematical terms, for all `a` and `b` in such a structure, `-a + b = b - a`.
More concisely: For any type `α` with a `SubtractionCommMonoid` structure, subtraction is commutative, that is, `-a + b = b - a` for all `a, b` in `α`.
|
div_mul_eq_mul_div
theorem div_mul_eq_mul_div : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a / b * c = a * c / b := by
sorry
This theorem states that for any type `α` that forms a commutative division monoid (which is a mathematical structure with operations of multiplication and division where multiplication is commutative), for any three elements `a`, `b`, and `c` of this type, the value obtained by dividing `a` by `b` and then multiplying the result by `c` is the same as the value obtained by multiplying `a` by `c` and then dividing the result by `b`. This property corresponds to the algebraic rule (a/b) * c = a * c / b.
More concisely: For any commutative division monoid type `α` and elements `a, b, c` of `α`, the expression `(a / b) * c` equals `(a * c) / b`.
|
neg_sub_neg
theorem neg_sub_neg : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -a - -b = b - a
This theorem, `neg_sub_neg`, states that for any type `α` where `α` is a subtraction commutative monoid, the negative of a difference between any two elements `a` and `b` of `α` after negating `b` is equal to the difference of `b` and `a`. In mathematical notation, this would be written as `-a - -b = b - a`.
More concisely: For any commutative monoid `α` with subtraction operation `-`, we have `- (a - b) = b - a`.
|
inv_mul_eq_div
theorem inv_mul_eq_div : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), a⁻¹ * b = b / a
This theorem, named `inv_mul_eq_div`, states that for any Division Commutative Monoid type `α` and any two elements `a` and `b` of this type, the multiplication of the inverse of `a` and `b` is equal to the result of dividing `b` by `a`. In mathematical language, it asserts that $a^{-1} * b = \frac{b}{a}$ for any `a` and `b` in the Division Commutative Monoid.
More concisely: For any element `a` and `b` in a Division Commutative Monoid, `a^(-1) * b = b / a`.
|
zero_sub
theorem zero_sub : ∀ {G : Type u_3} [inst : SubNegMonoid G] (a : G), 0 - a = -a
This theorem named `zero_sub` states that for all types `G` (which are instances of the `SubNegMonoid` class) and for every element `a` of type `G`, the result of the operation "0 minus a" is equal to the negative of `a`. In mathematical terms, this is similar to saying that in any subtractive negation monoid, subtracting any element from zero yields the negation of that element, i.e., `0 - a = -a`.
More concisely: For all types `G` in the `SubNegMonoid` class and every element `a` in `G`, `0 - a = -a`.
|
add_sub_cancel'_right
theorem add_sub_cancel'_right : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a + (b - a) = b
This is a theorem in the context of an additive commutative group. For any pair of elements 'a' and 'b' in this group, the theorem states that if you subtract 'a' from 'b' and then add 'a', you get back 'b'. In mathematical notation, this is expressed as a + (b - a) = b. It is an alias of the theorem `add_sub_cancel`.
More concisely: For all elements 'a' and 'b' in an additive commutative group, 'a' + ( 'b' - 'a' ) = 'b'.
|
sub_add_sub_cancel
theorem sub_add_sub_cancel : ∀ {G : Type u_3} [inst : AddGroup G] (a b c : G), a - b + (b - c) = a - c
This theorem states that for any type `G` that is an additive group, for every three elements `a`, `b`, and `c` of `G`, subtracting `b` from `a` and adding the result to the subtraction of `c` from `b` gives the same result as subtracting `c` from `a`. In mathematical notation, this would be expressed as `(a - b) + (b - c) = a - c`. This is a property that holds in the context of all additive groups.
More concisely: For any additive group `G` and elements `a, b, c` in `G`, `(a - b) + (b - c) = a - c`.
|
sub_eq_iff_eq_add
theorem sub_eq_iff_eq_add : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a - b = c ↔ a = c + b
This theorem, `sub_eq_iff_eq_add`, states that for any type G which is an instance of an additive group, and for any elements a, b, and c of type G, the statement "a subtract b equals c" is equivalent to "a equals c added to b". Essentially, it's expressing that subtraction can be rephrased as the addition of the negation in the context of an additive group.
More concisely: For any additive group G and elements a, b, and c of G, the statements "a - b = c" and "a = b + c" are equivalent.
|
smul_ite
theorem smul_ite :
∀ {α : Type u_4} {β : Type u_5} [inst : SMul β α] (p : Prop) [inst_1 : Decidable p] (a b : α) (c : β),
(c • if p then a else b) = if p then c • a else c • b
This theorem states that for any given types `α` and `β`, if there's a scalar multiplication function between `β` and `α`, and a decidable proposition `p`, and instances `a` and `b` of `α` and `c` of `β`, then scalar multiplication distributes over the if-then-else statement based on proposition `p`. In other words, multiplying `c` with the result of the if-then-else operation on `a` and `b` (based on `p`) is the same as applying the if-then-else operation on the scalar multiplications of `c` with `a` and `b` (based on `p`).
More concisely: For any types `α` and `β` with a scalar multiplication function, and proposition `p` decidable over `α`, if `c ∈ β` and `a, b ∈ α`, then `c * (if h : p then a else b) = if h then (c * a) else (c * b)`.
|
add_right_injective
theorem add_right_injective :
∀ {G : Type u_3} [inst : Add G] [inst_1 : IsLeftCancelAdd G] (a : G), Function.Injective fun x => a + x
The theorem `add_right_injective` states that for any type `G` which has an addition operation (`Add G`) and the addition operation in `G` is left cancellative (`IsLeftCancelAdd G`), for any element `a` of type `G`, the function that maps `x` to `a + x` is injective. In other words, if adding a certain value to two different elements in `G` yields the same result, then the two original elements must have been the same.
More concisely: If `G` is a type with left cancellative addition, then the function `x => a + x` is an injection on `G`.
|
Mathlib.Algebra.Group.Basic._auxLemma.18
theorem Mathlib.Algebra.Group.Basic._auxLemma.18 :
∀ {G : Type u_3} [inst : InvolutiveNeg G] {a b : G}, (-a = -b) = (a = b)
This theorem, named `Mathlib.Algebra.Group.Basic._auxLemma.18`, states that for all types `G` that have an `InvolutiveNeg` structure (i.e., a type where the negation operation is its own inverse), if two elements `a` and `b` of type `G` exist, then the equality of the negations of `a` and `b` is equivalent to the equality of `a` and `b` themselves. In simpler terms, in such a group, if the negation of `a` equals the negation of `b`, then `a` must be equal to `b`, and vice versa.
More concisely: In a group with an InvolutiveNeg structure, the negation of two elements are equal if and only if the elements are equal.
|
inv_inj
theorem inv_inj : ∀ {G : Type u_3} [inst : InvolutiveInv G] {a b : G}, a⁻¹ = b⁻¹ ↔ a = b
This theorem, `inv_inj`, states that for any given type `G` that has an involutive inverse (denoted as `InvolutiveInv G`), for any two elements `a` and `b` of type `G`, the inverse of `a` being equal to the inverse of `b` implies that `a` is equal to `b`. Essentially, it's saying that the operation of taking an inverse is injective in the type `G` with an involutive inverse. This theorem applies to any group-like structure with an well-defined inverse operation.
More concisely: If `G` is a type with an involutive inverse and `a` and `b` are elements of `G` such that `Inv a = Inv b`, then `a = b`.
|
sub_add_sub_cancel'
theorem sub_add_sub_cancel' : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), a - b + (c - a) = c - b
This theorem states that for any type `G` that forms an additive commutative group, and any three elements `a`, `b`, and `c` of type `G`, the result of subtracting `b` from `a`, then adding the result of subtracting `a` from `c`, is the same as the result of subtracting `b` from `c`. In mathematical notation, this is stating that for all a, b, and c in an additive commutative group G, we have the equality a - b + (c - a) = c - b.
More concisely: For all elements a, b, and c in an additive commutative group G, the expression (a - b) + (c - a) is equal to c - b.
|
div_eq_mul_one_div
theorem div_eq_mul_one_div : ∀ {G : Type u_3} [inst : DivInvMonoid G] (a b : G), a / b = a * (1 / b)
This theorem states that for any type 'G' which forms a 'DivInvMonoid' (a mathematical structure with division and inversion operations that follow certain rules), the division of any two elements 'a' and 'b' of type 'G' is equal to the multiplication of 'a' and the reciprocal of 'b'. In simpler terms, it's saying that 'a divided by b' is the same as 'a times one divided by b', which is a familiar property from basic arithmetic.
More concisely: For any type 'G' forming a 'DivInvMonoid' and elements 'a' and 'b' in 'G', a / b = a * (inv b), where inv denotes the multiplicative inverse.
|
sub_add_cancel'
theorem sub_add_cancel' : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a - (a + b) = -b
This theorem, referred to as `sub_add_cancel'`, is an alias of `sub_add_cancel_left`. It states that for any type `G` that forms an additive commutative group, for any elements `a` and `b` of this group, subtracting `(a + b)` from `a` yields the additive inverse of `b`. In mathematical notation, this can be expressed as $a - (a + b) = -b$.
More concisely: For any additive commutative group (G, +), for all a, b ∈ G, a + b - a = b.
|
div_mul_comm
theorem div_mul_comm : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a / b * c = c / b * a
This theorem states that for any type `α` that is a Division Commutative Monoid, and for any three elements `a`, `b`, and `c` of this type, the operation of dividing `a` by `b`, then multiplying the result by `c`, is equivalent to the operation of dividing `c` by `b`, then multiplying the result by `a`. In other words, the order of `a` and `c` can be swapped in this combination of division and multiplication operations.
More concisely: For any Division Commutative Monoid `α`, and elements `a`, `b`, and `c` in `α`, `(a / b) * c = c / b * a`.
|
self_eq_add_right
theorem self_eq_add_right : ∀ {M : Type u} [inst : AddLeftCancelMonoid M] {a b : M}, a = a + b ↔ b = 0
This theorem states that for any Type `M` which forms an `AddLeftCancelMonoid`, for any two elements `a` and `b` of type `M`, `a` is equal to `a + b` if and only if `b` is equal to `0`. In other words, in a left-cancellable monoid, an element `a` only equals the sum of `a` and another element `b` when `b` is the additive identity (zero).
More concisely: In a left-cancelable monoid, an element is equal to the sum of that element and another element if and only if the latter is the additive identity.
|
sub_ne_zero_of_ne
theorem sub_ne_zero_of_ne : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, a ≠ b → a - b ≠ 0
This theorem states that for any type `α` that is a subtraction monoid, given any two elements `a` and `b` of this type, if `a` is not equal to `b`, then the result of subtracting `b` from `a` is not zero. A subtraction monoid is a type with an associated subtraction operation that satisfies certain properties such as closure under the operation and the existence of an identity element.
More concisely: For any subtraction monoid type `α` and elements `a`, `b` of `α` with `a ≠ b`, the subtraction `a - b` is non-zero.
|
one_div_one_div
theorem one_div_one_div : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α), 1 / (1 / a) = a
This theorem states that for all types `α` equipped with a division operation (i.e., `α` forms a division monoid), the double reciprocation of any value `a` of type `α` yields the original value `a`. In mathematical terms, this theorem asserts that for any `a` in a division monoid `α`, the equation $1 / (1 / a) = a$ holds.
More concisely: For any type `α` with a division operation, the double reciprocal of any `a` in `α` equals `a`: $1 / (1 / a) = a$.
|
sub_sub_self
theorem sub_sub_self : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a - (a - b) = b
This theorem states that for any type `G` that is an additive commutative group, and for any elements `a` and `b` of type `G`, the result of subtracting `a` from the difference of `a` and `b` is equal to `b`. Essentially, it is expressing the algebraic identity `a - (a - b) = b`. This holds true in any additive commutative group.
More concisely: In any additive commutative group, for all elements `a` and `b`, `a - (a - b) = b`.
|
mul_left_injective
theorem mul_left_injective :
∀ {G : Type u_3} [inst : Mul G] [inst_1 : IsRightCancelMul G] (a : G), Function.Injective fun x => x * a
This theorem states that for any type `G` that has a multiplication operation and satisfies the property of right cancellation, multiplication from the left by a fixed element `a` of type `G` is an injective function. In other words, if `x * a = y * a` then `x = y`. Here, right cancellation means that for any `x`, `y` and `a` in `G`, if `x * a = y * a`, then `x = y`.
More concisely: For any type `G` with right cancellation and multiplication operation, multiplication by a fixed element `a` from the left is an injection.
|
mul_inv
theorem mul_inv : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), (a * b)⁻¹ = a⁻¹ * b⁻¹
The theorem `mul_inv` states that for any division commutative monoid `α` and any elements `a` and `b` from `α`, the inverse of the product of `a` and `b` is equal to the product of the inverse of `a` and the inverse of `b`. In other words, taking the inverse of a product is the same as taking the product of the inverses. This is expressed in the language of mathematics as `(a * b)⁻¹ = a⁻¹ * b⁻¹`.
More concisely: For any commutative monoid `α` and elements `a, b` in `α`, `(a * b)⁻¹ = a⁻¹ * b⁻¹`.
|
comp_add_left
theorem comp_add_left :
∀ {α : Type u_1} [inst : AddSemigroup α] (x y : α),
((fun x_1 => x + x_1) ∘ fun x => y + x) = fun x_1 => x + y + x_1
This theorem, `comp_add_left`, asserts that for any two elements `x` and `y` in an additive semigroup, the composition of two addition functions, the first adding `y` to its argument and the second adding `x` to the result, is equivalent to a single addition function that adds `x + y` to its argument. In terms of standard mathematical notation, this can be expressed as for all `x` and `y` in the semigroup `(x + (y + z)) = ((x + y) + z)`, where `z` is the input to the function. This is essentially a statement of associativity for the addition operation in the semigroup.
More concisely: For any additive semigroup and all elements `x` and `y`, the function `(λ (z : _), x + (y + z))` equals the function `(λ (z : _), (x + y) + z)`.
|
mul_div_cancel'_right
theorem mul_div_cancel'_right : ∀ {G : Type u_3} [inst : CommGroup G] (a b : G), a * (b / a) = b
This theorem, named `mul_div_cancel'_right`, is applicable to any type `G` that forms a commutative group (indicated by `CommGroup G`). It states that for any two elements `a` and `b` of the group, the product of `a` and the fraction `b / a` is equal to `b`. In mathematical notation, this theorem asserts that for all `a` and `b` in `G`, `a * (b / a) = b`. This theorem is an alias for another theorem named `mul_div_cancel`.
More concisely: For any commutative group `G` and elements `a, b` in `G`, `a * (b / a) = b`.
|
div_inv_eq_mul
theorem div_inv_eq_mul : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b : α), a / b⁻¹ = a * b
This theorem states that for any type `α` that is a division monoid, and for any two elements `a` and `b` of that type, the quotient of `a` by the inverse of `b` (`b⁻¹`) is equal to the product of `a` and `b`. In mathematical terms, it says that for all `a` and `b` in `α`, `a / b⁻¹ = a * b`.
More concisely: For any division monoid `α`, the quotient of `a` by the inverse of `b` equals the product of `a` and `b`, i.e., `a / b⁻¹ = a * b`.
|
inv_eq_one
theorem inv_eq_one : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a : α}, a⁻¹ = 1 ↔ a = 1
This theorem, named `inv_eq_one`, states that for any type `α` that has a division monoid structure, an element `a` of this type has the property that its inverse `a⁻¹` equals `1` if and only if `a` itself equals `1`. In other words, in a division monoid, only the element `1` has `1` as its inverse.
More concisely: In a division monoid, an element has an inverse equal to 1 if and only if it is the identity element 1.
|
neg_ne_zero
theorem neg_ne_zero : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, -a ≠ 0 ↔ a ≠ 0
This theorem, named `neg_ne_zero`, states that for any type `α` that is a subtraction monoid, a value `a` of that type has its negation not equal to zero if and only if `a` itself is not equal to zero. In other words, `-a` is not zero if and only if `a` is not zero, for all `a` in a subtraction monoid.
More concisely: For any subtraction monoid type `α`, the negation of a non-zero element `a` is not zero.
|
eq_inv_of_mul_eq_one_right
theorem eq_inv_of_mul_eq_one_right : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a b : α}, a * b = 1 → b = a⁻¹ := by
sorry
This theorem states that for any type `α` which forms a division monoid and any elements `a` and `b` of `α`, if `a` multiplied by `b` equals 1, then `b` is equal to the multiplicative inverse of `a`. Simply put, it's a property of division monoids (structures with multiplication, 1 and inversion where multiplication is associative and each element has an inverse) that when a product of two elements equals the identity element (1), the second element must be the inverse of the first.
More concisely: In a division monoid, if the product of two elements is the identity, then they are multiplicative inverses.
|
add_left_comm
theorem add_left_comm : ∀ {G : Type u_3} [inst : AddCommSemigroup G] (a b c : G), a + (b + c) = b + (a + c)
This theorem, `add_left_comm`, states that for any type `G` that forms an additive commutative semigroup, for any three elements `a`, `b`, and `c` of type `G`, the operation of addition is left-commutative. In other words, adding `a` to the sum of `b` and `c` (`a + (b + c)`) results in the same value as adding `b` to the sum of `a` and `c` (`b + (a + c)`). This property holds for all instances of `a`, `b`, and `c` in the commutative semigroup `G`.
More concisely: For any additive commutative semigroup `G`, the operation `+` is left-commutative, i.e., `a + (b + c) = b + (a + c)` for all `a, b, c` in `G`.
|
comp_add_right
theorem comp_add_right :
∀ {α : Type u_1} [inst : AddSemigroup α] (x y : α),
((fun x_1 => x_1 + x) ∘ fun x => x + y) = fun x_1 => x_1 + (y + x)
This theorem states that for any type `α` that is an additive semigroup, and for any elements `x` and `y` of that type, composing two addition operations on the right by `x` and `y` respectively, is equivalent to a single addition on the right by the sum of `y` and `x`. In mathematical terms, for any `x_1` in `α`, we have `(x_1 + y) + x = x_1 + (y + x)`.
More concisely: For any additive semigroup type `α` and elements `x, y` in `α`, `(x + y) = y + x`.
|
add_eq_zero_iff_eq_neg
theorem add_eq_zero_iff_eq_neg : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a + b = 0 ↔ a = -b
This theorem states that for any type `G` that forms an additive group, for any two elements `a` and `b` of `G`, the sum of `a` and `b` equals zero if and only if `a` equals the additive inverse of `b`. In mathematical terms, this is expressed as `a + b = 0` if and only if `a = -b`. This is a key property in the theory of additive groups.
More concisely: For any additive group `G` and elements `a, b` in `G`, `a + b = 0` if and only if `a = -b`.
|
mul_right_inj
theorem mul_right_inj :
∀ {G : Type u_3} [inst : Mul G] [inst_1 : IsLeftCancelMul G] (a : G) {b c : G}, a * b = a * c ↔ b = c
This theorem, `mul_right_inj`, states that for any type `G` that supports multiplication (`Mul G`) and has the cancellation property for multiplication on the left (`IsLeftCancelMul G`), for any elements `a`, `b`, and `c` of `G`, the equality `a * b = a * c` implies `b = c`. In other words, if multiplying `a` with `b` and `c` results in the same product, then `b` and `c` must be equal, given that the multiplication operation in `G` is left-cancellable.
More concisely: If `G` is a type with left-cancellative multiplication, then `a * b = a * c` implies `b = c`.
|
eq_neg_of_add_eq_zero_right
theorem eq_neg_of_add_eq_zero_right : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, a + b = 0 → b = -a := by
sorry
This theorem states that for any type `α` which is a subtraction monoid, for any two elements `a` and `b` of this type, if the sum of `a` and `b` equals zero, then `b` equals the negation of `a`. In mathematical terms, this can be written as: for all `a` and `b` in some type which is a subtraction monoid, if `a + b = 0`, then `b = -a`.
More concisely: If `α` is a subtraction monoid type, then for all `a` and `b` in `α`, if `a + b = 0`, then `b = -a`.
|
Mathlib.Algebra.Group.Basic._auxLemma.6
theorem Mathlib.Algebra.Group.Basic._auxLemma.6 :
∀ {M : Type u} [inst : AddLeftCancelMonoid M] {a b : M}, (a + b = a) = (b = 0)
This theorem, `Mathlib.Algebra.Group.Basic._auxLemma.6`, states that for any type `M` that is an instance of `AddLeftCancelMonoid`, for any elements `a` and `b` of `M`, the statement `a + b = a` is equivalent to the statement `b = 0`. In other words, in a left-cancellable monoid, when the sum of two elements `a` and `b` equals `a`, that means `b` must be the identity element of the monoid (which is `0` in the case of an additive monoid).
More concisely: In a left-cancelable monoid, for all elements `a` and `b`, `a + b = a` implies `b = 0`.
|
inv_comp_inv
theorem inv_comp_inv : ∀ (G : Type u_3) [inst : InvolutiveInv G], Inv.inv ∘ Inv.inv = id
The theorem `inv_comp_inv` states that for any type `G` that has an involutive inverse structure, the composition of the inverse operation performed twice (`Inv.inv ∘ Inv.inv`) is equivalent to the identity function (`id`). In other words, applying the inverse operation twice to any element returns the original element, which is a property characteristic of involutive operations.
More concisely: For any type `G` with an involutive inverse structure, `Inv.inv ∘ Inv.inv` equals the identity function `id`.
|
mul_div
theorem mul_div : ∀ {G : Type u_3} [inst : DivInvMonoid G] (a b c : G), a * (b / c) = a * b / c
This theorem states that for any type `G` that has a `DivInvMonoid` structure (which is a mathematical structure with division and inverse operations), and for any three elements `a`, `b`, and `c` of `G`, the result of multiplying `a` with the division of `b` by `c` (`a * (b / c)`) is the same as the result of dividing the product of `a` and `b` by `c` (`a * b / c`). This captures the concept of left-distributivity of multiplication over division.
More concisely: For any type `G` with a `DivInvMonoid` structure and any elements `a`, `b`, and `c` in `G`, we have `(a * (b / c)) = (a * b) / c`.
|
eq_inv_mul_of_mul_eq
theorem eq_inv_mul_of_mul_eq : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, b * a = c → a = b⁻¹ * c
This theorem states that for any group `G` and given group elements `a`, `b`, and `c`, if the product of `b` and `a` equals `c`, then `a` is equal to the product of the inverse of `b` and `c`. Here, `b⁻¹` denotes the inverse of `b` in the group `G`. This theorem captures a key property of groups in abstract algebra.
More concisely: If `a`, `b`, and `c` are group elements such that `b * a = c`, then `a = b⁻¹ * c`.
|
neg_surjective
theorem neg_surjective : ∀ {G : Type u_3} [inst : InvolutiveNeg G], Function.Surjective Neg.neg
This theorem, named `neg_surjective`, states that for any type `G` with an `InvolutiveNeg` structure (meaning negation on `G` is an involution, i.e., applying it twice gives back the original element), the negation function `Neg.neg` is surjective. In other words, every element of type `G` can be expressed as the negation of some other element in `G`. This is typically true in structures like groups, rings, and fields where each element has an additive inverse.
More concisely: For any type `G` equipped with an InvolutiveNeg structure, the negation function `Neg.neg` is a surjection.
|
mul_right_injective
theorem mul_right_injective :
∀ {G : Type u_3} [inst : Mul G] [inst_1 : IsLeftCancelMul G] (a : G), Function.Injective fun x => a * x
The theorem `mul_right_injective` states that, for any type `G` equipped with a multiplication operation and the property of left cancellation, multiplication on the right by a fixed element `a` from `G` is an injective function. In other words, if we consider the function `f(x) = a * x` where `*` represents the multiplication operation, then for all `x` and `y` in `G`, if `a * x = a * y` then `x = y`. This depends on the property of left cancellation, which asserts that for all `x`, `y`, and `z` in `G`, if `x * y = x * z` then `y = z`.
More concisely: If `G` is a type equipped with multiplication and left cancellation, then right multiplication by a fixed element `a` from `G` is an injective function. That is, for all `x` and `y` in `G`, if `a * x = a * y` then `x = y`.
|
mul_div_cancel
theorem mul_div_cancel : ∀ {G : Type u_3} [inst : CommGroup G] (a b : G), a * (b / a) = b
This theorem states that for any type `G` that is a commutative group, for any elements `a` and `b` of this group, the product of `a` and the division of `b` by `a` equals `b`. It implies that the operations of multiplication and division in this group cancel out each other. This is a generalization of the familiar property in arithmetic where multiplying a number by another number's division by the first number gives back the second number (i.e., `a * (b / a) = b`).
More concisely: For any commutative group `G` and elements `a` and `b` in `G`, `a * (b / a) = b`.
|
div_one
theorem div_one : ∀ {G : Type u_3} [inst : DivInvOneMonoid G] (a : G), a / 1 = a
This theorem states that for any type `G` that forms a `DivInvOneMonoid` (a mathematical structure that combines aspects of a monoid, a group, and a ring with division and a multiplicative identity element 'one'), the division of any element `a` of type `G` by the identity element 'one' is equal to the element `a` itself. In essence, it's encapsulating the common mathematical truth that any number divided by one remains the same.
More concisely: For any type `G` that is a `DivInvOneMonoid`, the operation of dividing an element `a` by the identity element 'one' results in `a` itself. In mathematical notation: `a / one = a` for all `a` in `G`.
|
sub_eq_of_eq_add'
theorem sub_eq_of_eq_add' : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c : G}, a = b + c → a - b = c
This theorem states that for any type `G` which is an instance of `AddCommGroup` (i.e., it's a group under commutative addition), given any three elements `a`, `b`, and `c` of this type, if `a` is equal to the sum of `b` and `c` (`a = b + c`), then the difference of `a` and `b` (`a - b`) is equal to `c`. This is a property of subtraction in the context of a commutative additive group.
More concisely: In a commutative additive group, if `a = b + c`, then `a - b = c`.
|
eq_add_of_sub_eq
theorem eq_add_of_sub_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a - c = b → a = b + c
This theorem states that for any type `G` that has an `AddGroup` structure, given any three elements `a`, `b`, and `c` of this type, if `a - c` equals `b`, then `a` equals `b + c`. In more mathematical terms, it says that in any additive group, if the difference of two elements equals a third element, then the first element equals the sum of the third element and the second one. It's essentially a re-arrangement of the standard equation `a - c = b` into the form `a = b + c`.
More concisely: In any additive group, if the difference of two elements is equal to a third element, then the first element is equal to the sum of the third element and the second one.
|
sub_ne_zero
theorem sub_ne_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a - b ≠ 0 ↔ a ≠ b
This theorem, `sub_ne_zero`, states that for any type `G` that is an additive group, the difference between any two elements `a` and `b` of `G` is not equal to zero if and only if `a` is not equal to `b`. In other words, within any additive group, if two elements are not equal, their difference won't be zero and conversely, if their difference is non-zero, the two elements are distinct.
More concisely: For any additive group G and all elements a, b in G, a ≠ b if and only if a - b ≠ 0.
|
add_left_injective
theorem add_left_injective :
∀ {G : Type u_3} [inst : Add G] [inst_1 : IsRightCancelAdd G] (a : G), Function.Injective fun x => x + a
The theorem `add_left_injective` states that for any type `G` which has an addition operation and possesses the right cancellation property with respect to addition, the function that adds a fixed element `a` from `G` to its input is injective. In other words, if for any two elements `x` and `y` of `G`, `x + a = y + a` implies `x = y`. This theorem essentially captures the idea that if adding a certain number doesn't change the uniqueness of the sum, then the original numbers were unique.
More concisely: For any additive type `G` with right cancellation property, the function `x => x + a` is injective.
|
Mathlib.Algebra.Group.Basic._auxLemma.10
theorem Mathlib.Algebra.Group.Basic._auxLemma.10 :
∀ {M : Type u} [inst : AddRightCancelMonoid M] {a b : M}, (a + b = b) = (a = 0)
This theorem, from the Mathlib library in the Algebra.Group.Basic module, is about right-cancellable monoids. Specifically, it states that for any type `M` which has the structure of a right-cancellable monoid (denoted by `AddRightCancelMonoid M`), and any two elements `a` and `b` of `M`, the equation `a + b = b` is true if and only if `a = 0`. In other words, adding `a` to `b` only results in `b` if `a` is the zero element in the monoid.
More concisely: For any right-cancellable monoid `M`, the equation `a +b = b` holds if and only if `a = 0`.
|
neg_sub'
theorem neg_sub' : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -(a - b) = -a - -b
This theorem states that for any given type `α` that forms a subtraction commutative monoid (a mathematical structure with a defined subtraction operation that is both associative and commutative), the negation of the difference between two elements `a` and `b` of that type is equal to the difference between the negation of `a` and the double negation of `b`. Specifically, it states that `-(a - b) = -a - -b` for all `a` and `b` in `α`.
More concisely: For any commutative subtraction monoid type `α`, the negation of `a - b` equals `-a - (-b)` for all `a` and `b` in `α`.
|
div_eq_iff_eq_mul
theorem div_eq_iff_eq_mul : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a / b = c ↔ a = c * b
This is a theorem about the properties of division and multiplication in a group. Specifically, for any type `G` that forms a group, and for any three elements `a`, `b`, and `c` of this group, the statement `a / b = c` is equivalent to the statement `a = c * b`. In other words, in a group, dividing `a` by `b` to get `c` is the same as multiplying `b` by `c` to get `a`.
More concisely: In a group, for all elements a, b, and c, the equality a / b = c holds if and only if a = c * b.
|
eq_of_div_eq_one
theorem eq_of_div_eq_one : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a b : α}, a / b = 1 → a = b
This theorem, `eq_of_div_eq_one`, states that for any type `α` with a division monoid structure, if the division of two elements `a` and `b` of that type equals 1, then `a` is equal to `b`. In other words, if `a / b = 1` then `a = b`. This is a general principle in division-based algebraic structures, reflecting the fact that 1 is the identity element for multiplication.
More concisely: If `α` is a type with a division monoid structure and `a / b = 1`, then `a = b`.
|
sub_sub_eq_add_sub
theorem sub_sub_eq_add_sub : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b c : α), a - (b - c) = a + c - b := by
sorry
The theorem `sub_sub_eq_add_sub` states that for any type `α` that forms a subtraction monoid (i.e., a set equipped with an associative binary operation and an identity element), and for any three elements `a`, `b`, and `c` of this type, the operation of subtracting `b - c` from `a` is equivalent to adding `c` to `a` and then subtracting `b`. In mathematical notation, this can be written as `a - (b - c) = a + c - b`.
More concisely: For any type `α` forming a subtraction monoid and any elements `a`, `b`, and `c` of `α`, `a - (b - c)` is equivalent to `a + c - b`.
|
sub_add_cancel
theorem sub_add_cancel : ∀ {G : Type u_3} [inst : AddGroup G] (a b : G), a - b + b = a
This theorem, `sub_add_cancel`, states that for any type `G` that forms an additive group, for any two elements `a` and `b` of that type, subtracting `b` from `a` and then adding `b` back results in `a`. In mathematical terms, this is expressing the identity `a - b + b = a` for all `a` and `b` in an additive group `G`.
More concisely: For all additive groups `G` and elements `a, b` in `G`, `a - b + b = a`.
|
eq_sub_of_add_eq
theorem eq_sub_of_add_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a + c = b → a = b - c
This theorem states that for all types `G` that have an `AddGroup` structure, and for any three elements `a`, `b`, and `c` of `G`, if `a + c` is equal to `b`, then `a` is equal to `b - c`. In other words, this theorem is a statement about the algebra of groups: if adding an element `c` to `a` gives `b`, you can get `a` back by subtracting `c` from `b`.
More concisely: If `a`, `b`, and `c` are elements of a group `G` with `AddGroup` structure such that `a + c = b`, then `a = b - c`.
|
sub_add_sub_comm
theorem sub_add_sub_comm :
∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c d : α), a - b + (c - d) = a + c - (b + d)
This theorem, `sub_add_sub_comm`, states that for any type `α` that forms a subtraction commutative monoid, the operation of subtracting `b` from `a`, adding the result to the difference of `c` and `d`, is equal to adding `a` and `c` first and then subtracting the sum of `b` and `d`. In mathematical terms, it states that for all `a`, `b`, `c`, and `d` in `α`, we have `a - b + (c - d) = a + c - (b + d)`.
More concisely: For any commutative subtraction monoid `α`, the operation `a - b + (c - d)` is equal to `a + c - (b + d)` for all `a, b, c, d ∈ α`.
|
bit1_zero
theorem bit1_zero : ∀ {M : Type u} [inst : AddMonoid M] [inst_1 : One M], bit1 0 = 1
This theorem, named `bit1_zero`, states that for any type `M` that has an addition operation (satisfying the properties of a monoid) and a distinct element called `one`, the `bit1` function applied to zero yields `one`. The `bit1` function is defined as the operation of doubling a given value (using addition) and then adding one. Therefore, when `bit1` is applied to zero, the result is `one`.
More concisely: For any monoid `M` with an element `one`, `bit1 0 = one`, where `bit1 x = x + x + 1`.
|
inv_injective
theorem inv_injective : ∀ {G : Type u_3} [inst : InvolutiveInv G], Function.Injective Inv.inv
The theorem `inv_injective` states that for any type `G` that carries the structure of `InvolutiveInv`, the inversion function `Inv.inv` is injective. In other words, if `G` is a type with involutive inversion (a mathematical operation where applying the operation twice returns the original value), then for all elements `a` and `b` in `G`, if the inverse of `a` is equal to the inverse of `b`, then `a` must equal `b`. The injection property ensures that different elements of `G` won't have the same inverse under `Inv.inv`.
More concisely: If `G` is a type with involutive inversion, then for all `a, b` in `G`, `Inv.inv a = Inv.inv b` implies `a = b`.
|
neg_eq_iff_eq_neg
theorem neg_eq_iff_eq_neg : ∀ {G : Type u_3} [inst : InvolutiveNeg G] {a b : G}, -a = b ↔ a = -b
This theorem states that for any given type `G` which has an involutive negation property (meaning that negating something twice returns the original thing), the negative of an element `a` from `G` being equal to another element `b` from `G` is logically equivalent to `a` being equal to the negative of `b`.
More concisely: For any type `G` with an involutive negation and elements `a` and `b` in `G`, `-a = b` is logically equivalent to `a = -b`.
|
eq_sub_iff_add_eq'
theorem eq_sub_iff_add_eq' : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c : G}, a = b - c ↔ c + a = b
This theorem states that for any three elements `a`, `b`, and `c` in an additive commutative group `G`, `a` equals `b` subtracted by `c` if and only if `c` added to `a` equals `b`. This theorem leverages the commutative and inverse properties of addition in such groups.
More concisely: For all elements `a`, `b`, and `c` in an additive commutative group, `a = b - c` if and only if `a + c = b`.
|
add_right_inj
theorem add_right_inj :
∀ {G : Type u_3} [inst : Add G] [inst_1 : IsLeftCancelAdd G] (a : G) {b c : G}, a + b = a + c ↔ b = c
This theorem, `add_right_inj`, states that for any type `G` that has an addition operation and the property of left-cancellative addition, for any elements `a`, `b`, and `c` of type `G`, the equality `a + b = a + c` is equivalent to `b = c`. In other words, if adding a certain element to two different elements yields the same result, then the two different elements must be equal. This is a property of left-cancellative operations in mathematics.
More concisely: If `G` is a type with left-cancellative addition, then for all `a`, `b`, `c` in `G`, `a + b = a + c` implies `b = c`.
|
div_mul_div_comm
theorem div_mul_div_comm :
∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c d : α), a / b * (c / d) = a * c / (b * d)
This theorem states that, for any type `α` that has a commutative division operation (i.e. a division in which the order of operands does not affect the result), and for any four elements `a`, `b`, `c`, and `d` of this type, the formula `(a / b) * (c / d) = (a * c) / (b * d)` holds true. In basic terms, it says that multiplication of two fractions (division expressions) is the same as multiplying the numerators (the top of the fractions) together and the denominators (the bottom of the fractions) together.
More concisely: For types `α` with commutative division, `(a / b) * (c / d) = (a * c) / (b * d)` for all `a, b, c, d ∈ α`.
|
sub_eq_iff_eq_add'
theorem sub_eq_iff_eq_add' : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c : G}, a - b = c ↔ a = b + c
This theorem states that for any type `G` that is an additive commutative group, given any three elements `a`, `b`, and `c` of the group `G`, `a` minus `b` equals `c` if and only if `a` equals `b` plus `c`. This is a property of additive commutative groups that connects the operation of subtraction with the operation of addition.
More concisely: For any additive commutative group G and elements a, b, and c in G, a - b = c if and only if a = b + c.
|
sub_right_inj
theorem sub_right_inj : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a - b = a - c ↔ b = c
The theorem `sub_right_inj` states that for all elements `a`, `b`, and `c` of an additive group `G`, the difference `a - b` equals `a - c` if and only if `b` equals `c`. Essentially, it asserts that subtracting the same value from two equal quantities leaves us with equal results.
More concisely: For all elements `a`, `b`, and `c` in an additive group `G`, `a - b = a - c` if and only if `b = c`.
|
Mathlib.Algebra.Group.Basic._auxLemma.2
theorem Mathlib.Algebra.Group.Basic._auxLemma.2 :
∀ {G : Type u_3} [inst : Add G] [inst_1 : IsLeftCancelAdd G] (a : G) {b c : G}, (a + b = a + c) = (b = c) := by
sorry
This theorem, `Mathlib.Algebra.Group.Basic._auxLemma.2`, states that for any type `G` that has an addition operation and satisfies the left cancellation property for addition, for any elements `a`, `b`, and `c` of `G`, the equality `a + b = a + c` implies `b = c`. In mathematical terms, this corresponds to the property that if adding a certain element on the left side of two other elements results in the same value, then those two elements are equal. This property is a key feature of structures that exhibit left cancellation.
More concisely: For any additive group `G`, if `a + b = a + c`, then `b = c`.
|
inv_eq_one_div
theorem inv_eq_one_div : ∀ {G : Type u_3} [inst : DivInvMonoid G] (x : G), x⁻¹ = 1 / x
This theorem states that for any given type `G` that is a division and inversion monoid, the inverse of any element `x` of this type is equal to the value obtained when `1` is divided by `x`. In other words, in the context of this specific type, the operation of finding an inverse and the operation of dividing `1` by an element are equivalent.
More concisely: For any type `G` being a division and inversion monoid, the inverse of an element `x` is equal to `1 / x`.
|
mul_mul_mul_comm
theorem mul_mul_mul_comm : ∀ {G : Type u_3} [inst : CommSemigroup G] (a b c d : G), a * b * (c * d) = a * c * (b * d)
This theorem, named `mul_mul_mul_comm`, states that for any type `G` that is a commutative semigroup, the sequence of multiplication between four elements `a`, `b`, `c`, and `d` can be rearranged without changing the result. More specifically, multiplying `a` and `b` and then multiplying the result by the product of `c` and `d` (`a * b * (c * d)`) results in the same value as multiplying `a` and `c` and then multiplying the result by the product of `b` and `d` (`a * c * (b * d)`). This property is a generalization of the commutative property of multiplication.
More concisely: For any commutative semigroup type `G`, the associativity of multiplication holds: `(a * b) * (c * d) = a * (b * c) * d`.
|
Mathlib.Algebra.Group.Basic._auxLemma.17
theorem Mathlib.Algebra.Group.Basic._auxLemma.17 :
∀ {G : Type u_3} [inst : InvolutiveInv G] {a b : G}, (a⁻¹ = b⁻¹) = (a = b)
This theorem, `Mathlib.Algebra.Group.Basic._auxLemma.17`, states that for any type `G` equipped with an `InvolutiveInv` (an operation that is its own inverse), and any two elements `a` and `b` of this type, the equality of their inverses (`a⁻¹ = b⁻¹`) is equivalent to the equality of the elements themselves (`a = b`). In other words, if two elements have the same inverse under this operation, they must be the same element.
More concisely: For any type `G` with an `InvolutiveInv`, if `a` and `b` are elements of `G` such that `a⁻¹ = b⁻¹`, then `a = b`.
|
sub_sub_cancel_left
theorem sub_sub_cancel_left : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a - b - a = -b
This theorem, `sub_sub_cancel_left`, states that for all values `a` and `b` that belong to some type `G`, which must be an additive commutative group, the result of subtracting `b` from `a`, and then subtracting `a` from the result, is equal to the additive inverse of `b`. In mathematical terms, this is saying that for any `a` and `b` in an additive commutative group `G`, we have `a - b - a = -b`.
More concisely: For all `a` and `b` in an additive commutative group `G`, we have `(a - b) - a = -b`.
|
sub_add_eq_sub_sub_swap
theorem sub_add_eq_sub_sub_swap : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b c : α), a - (b + c) = a - c - b
This theorem, named `sub_add_eq_sub_sub_swap`, states that for any type `α` that is a Subtraction Monoid, and given any three elements `a`, `b`, and `c` of that type, the result of subtracting the sum of `b` and `c` from `a` is the same as the result of subtracting `c` from `a` and then subtracting `b` from that result. In other words, it expresses a specific property of subtraction on a subtraction monoid: $a - (b + c) = a - c - b$.
More concisely: For any subtraction monoid type `α`, the subtraction is commutative over addition, that is, `a - (b + c) = a - c - b`.
|
sub_add
theorem sub_add : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - b + c = a - (b - c)
This theorem states that for any type `α` that is a subtraction commutative monoid, for any elements `a`, `b`, and `c` of type `α`, adding `c` to the result of subtracting `b` from `a` is equivalent to subtracting `b - c` from `a`. In mathematical terms, it says that for all `a`, `b`, and `c` in `α`, we have `a - b + c = a - (b - c)`. This expresses a specific property of subtraction and addition in the context of this particular type of algebraic structure.
More concisely: For any commutative subtraction monoid type `α` and elements `a`, `b`, and `c` in `α`, `a - b + c = a - (b - c)`.
|
add_neg_eq_zero
theorem add_neg_eq_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a + -b = 0 ↔ a = b
This theorem states that for any type `G` that forms an additive group, and any two elements `a` and `b` of `G`, the sum of `a` and the additive inverse of `b` is zero if and only if `a` and `b` are equal. In other words, in any additive group, the condition that `a` added to the negative of `b` equals zero is equivalent to `a` being equal to `b`.
More concisely: In an additive group, for all elements `a` and `b`, `a + (-b) = 0` if and only if `a = b`.
|
add_right_comm
theorem add_right_comm : ∀ {G : Type u_3} [inst : AddCommSemigroup G] (a b c : G), a + b + c = a + c + b
This theorem, named `add_right_comm`, states that for any type `G` that is an additive commutative semigroup, for any three elements `a`, `b`, and `c` of type `G`, the sum of `a`, `b`, and `c` remains the same even if the order of `b` and `c` is switched in the right-hand side of the sum. In mathematical notation, this is saying that for all `a`, `b`, and `c` in the semigroup `G`, `a + b + c = a + c + b`.
More concisely: For any additive commutative semigroup `G` and elements `a`, `b`, `c` in `G`, `a + b + c = a + c + b`.
|
Mathlib.Algebra.Group.Basic._auxLemma.20
theorem Mathlib.Algebra.Group.Basic._auxLemma.20 :
∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, (-a = 0) = (a = 0)
This theorem, named `_auxLemma.20` from the `Mathlib.Algebra.Group.Basic` module, states that for any type `α` that is a subtraction monoid and any element `a` of type `α`, `a` is zero if and only if `-a` is zero. In other words, in any subtraction monoid, the additive inverse of an element is zero if and only if the element itself is zero.
More concisely: In a subtraction monoid, an element and its additive inverse are equal to zero if and only if each other is zero.
|
bit1_add
theorem bit1_add :
∀ {M : Type u} [inst : AddCommSemigroup M] [inst_1 : One M] (a b : M), bit1 (a + b) = bit0 a + bit1 b
The theorem `bit1_add` states that for any type `M` that has an addition operation satisfying the commutative and associative laws (`AddCommSemigroup`) and also has an element designated as "one" (`One`), for any two elements `a` and `b` of that type, the operation `bit1` applied to the sum of `a` and `b` is equal to the sum of `bit0 a` and `bit1 b`. Here, `bit1 x` means `2*x + 1` and `bit0 x` means `2*x`.
More concisely: For any `AddCommSemigroup` type `M` with a `One` element, `bit1 (a + b) = bit0 a + bit1 b` for all `a, b ∈ M`.
|
div_mul_cancel
theorem div_mul_cancel : ∀ {G : Type u_3} [inst : Group G] (a b : G), a / b * b = a
This theorem, `div_mul_cancel`, states that for all elements `a` and `b` of a group `G`, the result of dividing `a` by `b` (written as `a / b`) and then multiplying by `b` is equal to `a`. This mirrors the similar property in the division of numbers where `(a / b) * b = a`, which holds true for any group structure.
More concisely: For all groups G and elements a, b in G, a / b * b = a.
|
eq_mul_inv_of_mul_eq
theorem eq_mul_inv_of_mul_eq : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a * c = b → a = b * c⁻¹
This theorem states that for any type `G` that forms a group, given three elements `a`, `b`, and `c` of this group, if the product of `a` and `c` equals `b`, then `a` is equal to the product of `b` and the inverse of `c`. In mathematical notation: if $a \cdot c = b$, then $a = b \cdot c^{-1}$. This theorem is a property of group theory, which is a fundamental concept in abstract algebra.
More concisely: If elements `a`, `b`, and `c` of a group `G` satisfy `a * c = b`, then `a = b * c^(-1)`.
|
Mathlib.Algebra.Group.Basic._auxLemma.3
theorem Mathlib.Algebra.Group.Basic._auxLemma.3 :
∀ {G : Type u_3} [inst : Mul G] [inst_1 : IsRightCancelMul G] (a : G) {b c : G}, (b * a = c * a) = (b = c) := by
sorry
This theorem states that for any type `G` that has a multiplication operation and satisfies the right cancellation law (i.e., if `x * a = y * a` then `x = y`), for any elements `a`, `b`, and `c` of `G`, `b` is equal to `c` if and only if the product of `b` and `a` is equal to the product of `c` and `a`. In other words, you can cancel `a` from both sides of the equation `b * a = c * a` to deduce `b = c`.
More concisely: For any type `G` with multiplication operation and right cancellation law, `b = c` if and only if `b * a = c * a`.
|
div_eq_one
theorem div_eq_one : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a / b = 1 ↔ a = b
This theorem, named `div_eq_one`, states that for any type `G` which forms a group (i.e., a set that has an associated operation satisfying certain properties), for any two elements `a` and `b` of this group, the quotient of `a` divided by `b` is equal to the identity element `1` if and only if `a` is equal to `b`. In other words, in a group, an element divided by another results in the identity only when those two elements are the same.
More concisely: In a group, for all elements `a` and `b`, `a / b = 1` if and only if `a = b`.
|
comp_mul_left
theorem comp_mul_left :
∀ {α : Type u_1} [inst : Semigroup α] (x y : α), ((fun x_1 => x * x_1) ∘ fun x => y * x) = fun x_1 => x * y * x_1
This theorem states that for any type `α` that forms a semigroup (that is, it has an associative multiplication operation), given any two elements `x` and `y` from `α`, the function that first multiplies by `y` and then by `x` (i.e., composition of multiplying by `y` and then by `x`) is equivalent to the function that multiplies by `x * y`. In terms of mathematical notation, this reads as `(x * (y * _)) = (x * y * _)` for all `_` in `α`, where `_` is a placeholder for the argument to the function.
More concisely: For any semigroup type `α` and elements `x, y` in `α`, the functions `x * (y * _)` and `(x * y) * _` are equal.
|
sub_zero
theorem sub_zero : ∀ {G : Type u_3} [inst : SubNegZeroMonoid G] (a : G), a - 0 = a
This theorem, named `sub_zero`, states that in any subtraction-negative-zero monoid `G` (a specific algebraic structure with subtraction and zero elements), subtracting zero from any element `a` of `G` results in `a` itself. In other words, for any given element in this subtraction-negative-zero monoid, subtracting zero does not change the value of the element. The theorem generalizes the common idea familiar from basic arithmetic where subtracting zero from any number leaves the number unchanged.
More concisely: In a subtraction-negative-zero monoid, subtracting zero from any element is the identity operation.
|
mul_right_eq_self
theorem mul_right_eq_self : ∀ {M : Type u} [inst : LeftCancelMonoid M] {a b : M}, a * b = a ↔ b = 1
The theorem `mul_right_eq_self` states that for any type `M` that is a Left Cancelable Monoid, and for any elements `a` and `b` of that type, the condition `a * b = a` is equivalent to `b = 1`. In the language of algebra, this theorem says that if the multiplication of `a` and `b` equals `a`, then `b` must be the identity element of the monoid, which is `1` in this context.
More concisely: For any left cancelable monoid M and its elements a and b, a * b = a if and only if b is the identity element 1.
|
comp_mul_right
theorem comp_mul_right :
∀ {α : Type u_1} [inst : Semigroup α] (x y : α),
((fun x_1 => x_1 * x) ∘ fun x => x * y) = fun x_1 => x_1 * (y * x)
This theorem states that for any type `α` that forms a semigroup, the composition of two multiplication functions, first multiplying by `y` and then multiplying by `x`, is equivalent to a single multiplication by the product of `y` and `x`. Specifically, for any elements `x` and `y` of the semigroup, the function that multiplies an input by `x` after it has been multiplied by `y` is the same as the function that multiplies an input by `y * x`.
More concisely: For any semigroup type `α`, the function `(×) x := λ (y : α), y × x` is equal to `(×) (x × y)` where `×` is the multiplication operation in `α`.
|
mul_div_assoc
theorem mul_div_assoc : ∀ {G : Type u_3} [inst : DivInvMonoid G] (a b c : G), a * b / c = a * (b / c)
This theorem states that for any type `G` that is a `DivInvMonoid`, and for any elements `a`, `b`, `c` of `G`, the operation of multiplication and division is associative. In other words, multiplying `a` and `b` first and then dividing the result by `c` is the same as first dividing `b` by `c` and then multiplying the result with `a`. In mathematical notation, this can be written as `(a * b) / c = a * (b / c)`.
More concisely: For any `DivInvMonoid` type `G` and elements `a`, `b`, `c` in `G`, `(a * b) / c = a * (b / c)`.
|
sub_add_cancel''
theorem sub_add_cancel'' : ∀ {G : Type u_3} [inst : AddGroup G] (a b : G), a - (b + a) = -b
This theorem, `sub_add_cancel''`, states that for any type `G` that forms an additive group, for any elements `a` and `b` of `G`, subtracting `b + a` from `a` results in `-b`. In mathematical terms, this can be denoted as `a - (b + a) = -b` for any `a, b` in `G`. Essentially, it's an alias for the theorem `sub_add_cancel_right` and it describes one of the properties of subtraction in additive groups.
More concisely: For any additive group `G` and elements `a, b` in `G`, `a - (b + a) = -b`.
|
add_sub_add_right_eq_sub
theorem add_sub_add_right_eq_sub : ∀ {G : Type u_3} [inst : AddGroup G] (a b c : G), a + c - (b + c) = a - b
This theorem states that for all types `G` that form an additive group, for any three elements `a`, `b`, and `c` of this type, the result of adding `c` to `a`, and then subtracting the result of adding `c` to `b`, is equal to the result of subtracting `b` from `a`. In mathematical notation, this would be represented as `a + c - (b + c) = a - b`.
More concisely: For all types `G` that form an additive group, the operation of adding and then subtracting is commutative, that is, `a + c - (b + c) = a - b` for all elements `a`, `b`, and `c` in `G`.
|
natAbs_nsmul_eq_zero
theorem natAbs_nsmul_eq_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a : G} {n : ℤ}, n.natAbs • a = 0 ↔ n • a = 0 := by
sorry
The theorem `natAbs_nsmul_eq_zero` states that for any type `G` which is an add group, and for any element `a` of `G` and integer `n`, the `n`-fold addition of `a` (defined by `n • a`) is zero if and only if the `n`-fold addition of `a` where `n` is the absolute value of an integer is zero. In other words, the repetition of addition operation (`n • a`) results in zero both when `n` is an integer and when `n` is the absolute value of that integer.
More concisely: For any add group `G` and element `a` in `G`, the repeated addition of `a` (`n • a`) is equal to zero if and only if the absolute value of the integer `n` equals zero. (In Lean, this theorem is named `natAbs_nsmul_eq_zero`.)
|
mul_div_cancel'''
theorem mul_div_cancel''' : ∀ {G : Type u_3} [inst : CommGroup G] (a b : G), a * b / a = b
This theorem, known as `mul_div_cancel'''`, states that for all types `G` that are commutative groups, for any two elements `a` and `b` in `G`, if you multiply `a` and `b` together and then divide the result by `a`, you get `b`. In mathematical notation, this can be written as $a * b / a = b$. This theorem is an alias of the theorem `mul_div_cancel_left`.
More concisely: For all commutative groups `G` and elements `a, b` in `G`, `a * b = a * c` implies `b = c`.
|
add_sub_add_comm
theorem add_sub_add_comm :
∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c d : α), a + b - (c + d) = a - c + (b - d)
This theorem, `add_sub_add_comm`, states that for any type `α` that is a commutative subtraction monoid, for any four elements `a`, `b`, `c` and `d` of type `α`, adding `b` to `a`, then subtracting the sum of `c` and `d` is equal to subtracting `c` from `a`, then adding the result to the difference of `b` and `d`. In mathematical notation, this is represented as \(a + b - (c + d) = a - c + (b - d)\). This theorem is a statement about the commutativity and associativity of addition and subtraction in such a type.
More concisely: For any commutative subtraction monoid type `α`, the commutative and associative properties of addition and subtraction imply that `a + b - (c + d) = a - c + (b - d)` for all `a, b, c, d ∈ α`.
|
neg_add'
theorem neg_add' : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -(a + b) = -a - b
This theorem, named `neg_add'`, states that for any type `α` that is a commutative monoid under subtraction (meaning subtraction can be applied in any order without changing the result), and for any two elements `a` and `b` of this type, the negation of the sum of `a` and `b` is equal to the result of subtracting `b` from the negation of `a`. In mathematical notation, this is saying that for all `a` and `b`, `-(a + b) = -a - b`.
More concisely: For any commutative monoid `α` under subtraction, the negation of the sum of two elements `a` and `b` equals the difference between the negations of `a` and `b`, i.e., `-(a + b) = -a - b`.
|
sub_sub_cancel
theorem sub_sub_cancel : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a - (a - b) = b
This theorem, `sub_sub_cancel`, states that for any type `G` that is an additive commutative group (denoted by `[inst : AddCommGroup G]`), for any two elements `a` and `b` of type `G`, if you subtract `b` from `a` and then subtract the result from `a` again, you end up with `b`. In mathematical notation, this can be written as `a - (a - b) = b` for all `a, b ∈ G`.
More concisely: For any additive commutative group `G` and elements `a, b` in `G`, `a - (a - b) = b`.
|
div_mul_cancel'
theorem div_mul_cancel' : ∀ {G : Type u_3} [inst : Group G] (a b : G), a / b * b = a
This theorem, known as an alias of `div_mul_cancel`, states that for any group `G` of a certain type and for any elements `a` and `b` in this group, the operation of dividing `a` by `b`, and then multiplying the result by `b`, will always equal `a`. This is a generalization of the principle from arithmetic that dividing a number by a certain factor and then multiplying the result by the same factor will restore the original number.
More concisely: For any group `G` and elements `a, b` in `G` such that `b ≠ 0`, we have `a / b * b = a`.
|
sub_eq_zero
theorem sub_eq_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a - b = 0 ↔ a = b
This theorem states that for any type `G` that is an additive group, the result of subtraction operation `a - b` is zero if and only if `a` and `b` are equal. In other words, within any additive group, the difference between two elements is zero exactly when those two elements are the same.
More concisely: In any additive group, for all elements `a` and `b`, `a - b = 0` if and only if `a = b`.
|
mul_div_right_comm
theorem mul_div_right_comm : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a * b / c = a / c * b := by
sorry
This theorem states that for any type `α` that is a Division Commutative Monoid, given three elements `a`, `b`, and `c` of this type, the product of `a` and `b` divided by `c` is equal to `a` divided by `c` multiplied by `b`. In other words, multiplication and division operations are commutative, so we can rearrange the order of these operations without changing the result. It's represented mathematically as: `a * b / c = a / c * b`.
More concisely: For any division commutative monoid type `α`, the law of dividing by the same element is commutative, that is, `a * b / c = a / c * b`.
|
inv_eq_iff_mul_eq_one
theorem inv_eq_iff_mul_eq_one : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a⁻¹ = b ↔ a * b = 1
This theorem states that for any type `G` that has a group structure, and any two elements `a` and `b` of this group, the inverse of `a` is equal to `b` if and only if the product of `a` and `b` is the identity element of the group. In mathematical terms, this is saying that for all $a, b \in G$, we have $a^{-1} = b$ if and only if $a*b = 1$, where $*$ denotes the group operation, $1$ is the identity element, and $a^{-1}$ is the inverse of $a$.
More concisely: For any group G and elements a, b in G, a^(-1) = b if and only if a * b = 1.
|
add_left_eq_self
theorem add_left_eq_self : ∀ {M : Type u} [inst : AddRightCancelMonoid M] {a b : M}, a + b = b ↔ a = 0
This theorem states that for any type `M` that is an `AddRightCancelMonoid`, given any two elements `a` and `b` of type `M`, the sum of `a` and `b` equals `b` if and only if `a` is zero. In other words, in the context of a monoid where the right cancellation law holds (i.e., for all `a`, `b`, and `c` in `M`, if `a + b = a + c`, then `b = c`), the only element `a` that when added to another element `b` equals `b`, is the zero element.
More concisely: For any AddRightCancelMonoid `M`, an element `a` of `M` satisfies `a + b = b` if and only if `a` is the zero element of `M`.
|
mul_div_cancel_left
theorem mul_div_cancel_left : ∀ {G : Type u_3} [inst : CommGroup G] (a b : G), a * b / a = b
This theorem states that for all elements `a` and `b` of any commutative group `G`, the result of multiplying `a` and `b` together and then dividing by `a` is equal to `b`. In other words, it says that if you multiply any element by another, and then divide the result by the original element, you get back the second element. This is essentially expressing the cancellation law of division in the context of commutative groups.
More concisely: For all commutative groups G and elements a, b in G, a \* b = b \* a implies a \* (b / a) = b.
|
mul_inv_eq_one
theorem mul_inv_eq_one : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a * b⁻¹ = 1 ↔ a = b
This theorem states that for any group `G` and any elements `a` and `b` of `G`, the product of `a` and the inverse of `b` is equal to the identity element `1` if and only if `a` is equal to `b`. In other words, in a group, an element times the inverse of another element equals the identity only when the two elements are the same.
More concisely: In a group, for all elements `a` and `b`, `a * b^(-1) = 1` if and only if `a = b`.
|
add_sub_sub_cancel
theorem add_sub_sub_cancel : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), a + b - (a - c) = b + c
This theorem states that for any type `G` which forms an additive commutative group, for any elements `a`, `b`, and `c` of this group, the result of subtracting `(a - c)` from `a + b` is equal to `b + c`. In other words, it expresses a certain symmetry property of addition and subtraction in an additive commutative group. The theorem is universal, meaning it holds for all such groups and all elements of these groups.
More concisely: For any additive commutative group (G : Type) and elements a, b, c of G, a + b = b + c + (-c).
|
sub_neg_eq_add
theorem sub_neg_eq_add : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b : α), a - -b = a + b
This theorem states that for any type `α` that forms a subtraction monoid, for any two elements `a` and `b` of that type, subtracting the negation of `b` from `a` is equal to adding `b` to `a`. In mathematical terms, this theorem encapsulates the idea that `a - (-b) = a + b`.
More concisely: For any type `α` that forms a subtraction monoid, `a - (-b) = a + b` for all `a, b` in `α`.
|
add_add_add_comm
theorem add_add_add_comm :
∀ {G : Type u_3} [inst : AddCommSemigroup G] (a b c d : G), a + b + (c + d) = a + c + (b + d)
This theorem states that for any type `G` that has an addition operation (and where this operation is commutative and associative, i.e., forms an addition commutative semigroup), for any four elements `a`, `b`, `c`, and `d` of `G`, the sum of `a`, `b`, `c`, and `d` is the same regardless of whether `b` and `c` are grouped together or `c` and `d` are grouped together. In other words, `a + b + (c + d)` is equal to `a + c + (b + d)`.
More concisely: For any commutative and associative addition semigroup `G`, the order of adding two elements does not affect the sum: `a + b + c = a + c + b` for all `a, b, c` in `G`.
|
one_div_one
theorem one_div_one : ∀ {G : Type u_3} [inst : DivInvOneMonoid G], 1 / 1 = 1
This theorem states that for any type `G` which has a `DivInvOneMonoid` structure (a structure that includes operations for division and inversion, along with the existence of an identity element 'one'), the division of 'one' by 'one' is always equal to 'one'. It generalizes the familiar rule in arithmetic that anything divided by itself is 'one' to any context where the concept of 'division', 'inversion', and 'one' make sense.
More concisely: For any type `G` with a `DivInvOneMonoid` structure, `one_div_one` equals `one`.
|
neg_eq_iff_add_eq_zero
theorem neg_eq_iff_add_eq_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, -a = b ↔ a + b = 0
This theorem, `neg_eq_iff_add_eq_zero`, states that for any type `G` that is an additive group, and for any elements `a` and `b` of `G`, the negation of `a` equals `b` if and only if the sum of `a` and `b` is zero. In simpler terms: in any additive group, the negative of a number is another number if adding the original number to the other number yields zero.
More concisely: In an additive group, for all elements `a` and `b`, `-a = b` if and only if `a + b = 0`.
|
neg_sub
theorem neg_sub : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b : α), -(a - b) = b - a
This theorem, named `neg_sub`, states that for all types `α` in an instance of a subtraction monoid, the negation of the difference of two elements `a` and `b` equals the difference of `b` and `a`. In other words, for any elements `a` and `b` in `α`, `- (a - b) = b - a`. This theorem captures the property of subtraction monoids that swapping the operands of subtraction and then negating the result gives the same outcome as the original subtraction operation.
More concisely: For all types `α` in a subtraction monoid and all `a, b` in `α`, `- (a - b) = b - a`.
|
bit0_zero
theorem bit0_zero : ∀ {M : Type u} [inst : AddMonoid M], bit0 0 = 0
The theorem `bit0_zero` states that for any type `M` that forms an additive monoid, the `bit0` of zero is equal to zero. In other words, if you add zero to itself in the context of the `bit0` function, you will always get zero. In mathematical terms, this can be expressed as `0 + 0 = 0`.
More concisely: For any additive monoid type M, `bit0 (0 : M) = 0`.
|
add_add_sub_cancel
theorem add_add_sub_cancel : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), a + c + (b - c) = a + b
This theorem states that for any additive commutative group `G` and any elements `a`, `b`, and `c` of `G`, the sum of `a` and `c` plus the difference between `b` and `c` equals the sum of `a` and `b`. In mathematical notation, this can be written as: `a + c + (b - c) = a + b`. The theorem highlights a property of subtraction in the context of additive commutative groups: subtracting an element and then adding it back effectively cancels the subtraction.
More concisely: In an additive commutative group, the sum of an element with another element and its negative is equal to the sum of the two original elements.
|
add_sub_cancel
theorem add_sub_cancel : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a + (b - a) = b
This theorem, `add_sub_cancel`, states that for any type `G` that is an additive commutative group (denoted by `AddCommGroup G`), for any two elements `a` and `b` of this type, the result of adding `a` to the difference of `b` and `a` (`a + (b - a)`) is always `b`. This is a basic property of subtraction in the context of additive commutative groups, reflecting the idea that adding a quantity and then subtracting the same quantity results in the original value.
More concisely: For any additive commutative group `G` and elements `a, b` in `G`, `a + (b - a) = b`.
|
add_sub_add_left_eq_sub
theorem add_sub_add_left_eq_sub : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), c + a - (c + b) = a - b := by
sorry
This theorem states that for any type `G` which is an instance of an additive commutative group, for any three elements `a`, `b`, and `c` of `G`, the equation `c + a - (c + b) = a - b` holds true. In other words, if you add `c` to `a` and subtract the sum of `c` and `b`, the result is the same as just subtracting `b` from `a`.
More concisely: For any additive commutative group `G` and elements `a`, `b`, `c` in `G`, `c + a - (c + b) = a - b`.
|
add_right_eq_self
theorem add_right_eq_self : ∀ {M : Type u} [inst : AddLeftCancelMonoid M] {a b : M}, a + b = a ↔ b = 0
This theorem, `add_right_eq_self`, states that for any type `M` which is an instance of `AddLeftCancelMonoid`, and any elements `a` and `b` of `M`, the equation `a + b = a` holds true if and only if `b` equals zero. In mathematical terms, for a left-cancelable monoid, adding an element `b` to `a` results in `a` only when `b` is the identity element of the monoid (which is zero in the case of addition).
More concisely: For any `M` an instance of `AddLeftCancelMonoid` and `a` an element of `M`, `a + b = a` if and only if `b` is the additive identity of `M`.
|
mul_left_comm
theorem mul_left_comm : ∀ {G : Type u_3} [inst : CommSemigroup G] (a b c : G), a * (b * c) = b * (a * c)
This theorem, `mul_left_comm`, states that for all types `G` that have an instance of the `CommSemigroup` structure, and for any three elements `a`, `b`, and `c` of type `G`, the operation of multiplying `a` with the result of multiplying `b` and `c` is equal to the operation of multiplying `b` with the result of multiplying `a` and `c`. In conventional mathematical terms, for any three elements in a commutative semigroup, the multiplication operation is left-commutative.
More concisely: For all types `G` with `CommSemigroup` structure and all elements `a`, `b`, `c` in `G`, `(a × b) = (b × a)`.
|
add_neg_eq_iff_eq_add
theorem add_neg_eq_iff_eq_add : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a + -b = c ↔ a = c + b
This theorem states that for any type `G` which is an additive group, and any elements `a`, `b` and `c` of `G`, the condition of `a` plus the additive inverse of `b` being equal to `c` is equivalent to `a` being equal to the sum of `c` and `b`. In mathematical terms, it expresses that in an additive group `G`, `a + (-b) = c` if and only if `a = c + b`.
More concisely: For any additive group `G` and elements `a`, `b` of `G`, `a + (-b) = c` if and only if `a = c + b`.
|
add_sub
theorem add_sub : ∀ {G : Type u_3} [inst : SubNegMonoid G] (a b c : G), a + (b - c) = a + b - c
This theorem, named `add_sub`, states that for all types `G` that form a subtractable negated monoid (as indicated by `SubNegMonoid G`), for any three elements `a`, `b`, and `c` of `G`, the result of adding `a` and the difference between `b` and `c` (`a + (b - c)`) is equal to the result of subtracting `c` from the sum of `a` and `b` (`a + b - c`). This is essentially the statement of the distributive property of subtraction over addition within a subtractable negated monoid structure.
More concisely: For any subtractable negated monoid type `G`, the distributive property holds: `a + (b - c) = a + b - c` for all elements `a, b, c` of `G`.
|
div_div_eq_mul_div
theorem div_div_eq_mul_div : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b c : α), a / (b / c) = a * c / b
This theorem, `div_div_eq_mul_div`, states that for any type α which forms a division monoid, for any three elements `a`, `b`, `c` of this type, the operation of dividing `a` by the result of `b / c` is equivalent to multiplying `a` and `c` and then dividing the result by `b`. Formally in mathematical terms, it asserts that $\frac{a}{\frac{b}{c}} = \frac{a \cdot c}{b}$.
More concisely: For any type α forming a division monoid, $\frac{a}{\frac{b}{c}} = \frac{a \cdot c}{b}$.
|
sub_eq_neg_add
theorem sub_eq_neg_add : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), a - b = -b + a
This theorem states that for any type `α` that is a commutative monoid under subtraction ( a mathematical structure with a single associative binary operation and an identity element), the operation of subtracting `b` from `a` (represented as `a - b`) is the same as the operation of adding the negative of `b` to `a` (represented as `-b + a`). This holds true for any elements `a` and `b` of type `α`.
More concisely: For any commutative monoid `α` with respect to subtraction, for all `a, b` in `α`, `a - b` is equivalent to `a + (-b)`.
|
eq_mul_inv_iff_mul_eq
theorem eq_mul_inv_iff_mul_eq : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a = b * c⁻¹ ↔ a * c = b
This theorem states that for any group `G` and any elements `a`, `b`, `c` of `G`, `a` is equal to the product of `b` and the inverse of `c` if and only if `a` multiplied by `c` is equal to `b`. In other words, it states an equivalence between two ways of expressing a relationship involving multiplication and inversion in a group.
More concisely: For any group `G` and elements `a`, `b`, `c` in `G`, `a = b * c^-1` if and only if `a * c = b`.
|
ite_smul
theorem ite_smul :
∀ {α : Type u_4} {β : Type u_5} [inst : SMul β α] (p : Prop) [inst_1 : Decidable p] (a : α) (b c : β),
(if p then b else c) • a = if p then b • a else c • a
This theorem, named `ite_smul`, is a property of the scalar multiplication operation in some arbitrary types `α` and `β`. Given a proposition `p` that can be decided, and elements `a` of type `α`, `b` of type `β`, and `c` of type `β`, the theorem states that the scalar multiplication of the conditional value (if `p` then `b` else `c`) with `a` is the same as the conditional value of the scalar multiplication (if `p` then `b • a` else `c • a`). In other words, the scalar multiplication operation can be "distributed" over a conditional statement.
More concisely: For all propositions `p`, types `α` and `β`, and elements `a` of type `α` and `b`, `c` of type `β`, if `p` can be decided, then `(if p then b else c) • a = if p then (b • a) else (c • a)`.
|
Mathlib.Algebra.Group.Basic._auxLemma.1
theorem Mathlib.Algebra.Group.Basic._auxLemma.1 :
∀ {G : Type u_3} [inst : Mul G] [inst_1 : IsLeftCancelMul G] (a : G) {b c : G}, (a * b = a * c) = (b = c) := by
sorry
This theorem, `Mathlib.Algebra.Group.Basic._auxLemma.1`, states that for any type `G` that has a multiplication operation (`Mul G`) and where multiplication is left-cancellable (`IsLeftCancelMul G`), given any element `a` of type `G` and any two elements `b` and `c` of type `G`, the equality `a * b = a * c` implies `b = c`. In other words, if multiplying `a` by `b` results in the same product as multiplying `a` by `c`, then `b` must be equal to `c`. This is a property of left-cancellation in multiplication.
More concisely: If `G` is a type with left-cancellable multiplication, then `a * b = a * c` implies `b = c` for all `a, b, c` in `G`.
|
mul_left_eq_self
theorem mul_left_eq_self : ∀ {M : Type u} [inst : RightCancelMonoid M] {a b : M}, a * b = b ↔ a = 1
This theorem, `mul_left_eq_self`, states that for any type `M` that forms a right cancelable monoid (a type of algebraic structure), and any two elements `a` and `b` of `M`, the equation `a * b = b` holds if and only if `a` equals 1. In mathematical notation, this would be written as ∀a, b ∈ M, a * b = b ↔ a = 1. This means that multiplying an element by another is the same as the second element itself only when the first element is the identity element of the monoid (in this case, 1).
More concisely: For any right cancelable monoid M and elements a, b in M, a * b = b if and only if a is the identity element 1.
|
eq_sub_iff_add_eq
theorem eq_sub_iff_add_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a = b - c ↔ a + c = b
This theorem states that for any type `G` that forms an Additive Group, given any three elements `a`, `b`, and `c` in `G`, `a` equals the difference of `b` and `c` if and only if `b` is the sum of `a` and `c`. In essence, it is a property of the additive group that allows us to rearrange an equation involving subtraction into an equivalent equation involving addition. In terms of formal math, it's stating the equivalence between the two expressions `a = b - c` and `a + c = b`.
More concisely: For any additive group `G` and elements `a, b, c` in `G`, `a = b - c` if and only if `a + c = b`.
|
mul_right_comm
theorem mul_right_comm : ∀ {G : Type u_3} [inst : CommSemigroup G] (a b c : G), a * b * c = a * c * b
The theorem `mul_right_comm` states that for any type `G` that is a commutative semigroup, and for any three elements `a`, `b`, and `c` of this type, the statement `a * b * c = a * c * b` holds true. In other words, within a commutative semigroup, if you multiply three elements together, the result stays the same even if you swap the last two elements.
More concisely: In a commutative semigroup, the order of multiplication of three elements does not affect the result: `a * b * c = a * c * b`.
|
additive_of_isTotal
theorem additive_of_isTotal :
∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid β] (r : α → α → Prop) [inst_1 : IsTotal α r] (f : α → α → β)
(p : α → Prop),
(∀ {a b : α}, p a → p b → f a b + f b a = 0) →
(∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b + f b c) →
∀ {a b c : α}, p a → p b → p c → f a c = f a b + f b c
This theorem states that if you have a binary function, `f`, from a type `α` (which is equipped with a total relation `r`) to an additive monoid `β`, and this function is anti-symmetric (i.e., `f a b + f b a = 0`), then you can show that this function is additive (meaning it satisfies `f a c = f a b + f b c`) by assuming that `r a b` and `r b c` are true. This can be restricted to a subset specified by a predicate `p`.
In other words, if `f` is an anti-symmetric binary function defined on a subset of a totally ordered set subject to a predicate `p`, then `f` is also additive on this subset under the total order.
More concisely: If `f` is an anti-symmetric function from a subset `α` of a totally ordered set equipped with a relation `r` to an additive monoid, then `f` is additive on `α` under `r` when `r` holds for arguments `a`, `b`, and `c` satisfying `p(a)`, `p(b)`, and `p(c)`.
|
add_sub_assoc
theorem add_sub_assoc : ∀ {G : Type u_3} [inst : SubNegMonoid G] (a b c : G), a + b - c = a + (b - c)
This theorem, named `add_sub_assoc`, states that for any given type 'G' that is a SubNegMonoid (a certain mathematical structure), for any three elements 'a', 'b', and 'c' of this type 'G', the operation of adding 'b' to 'a', and from the result subtracting 'c' (expressed as `a + b - c`), is equal to the operation of subtracting 'c' from 'b', and then adding the result to 'a' (expressed as `a + (b - c)`). This is an associative property between addition and subtraction in the context of a SubNegMonoid.
More concisely: For any SubNegMonoid type 'G' and elements 'a', 'b', 'c' in 'G', the expression 'a + (b - c)' equals '(a + b) - c'.
|
eq_add_neg_of_add_eq
theorem eq_add_neg_of_add_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a + c = b → a = b + -c
This theorem states that for any type `G` which has an `AddGroup` structure, and for any elements `a`, `b`, and `c` of `G`, if `a + c` equals `b`, then `a` equals `b` plus the additive inverse of `c`. In other words, if the sum of two elements in the group is equal to a third element, then the first element is equal to the difference between the third element and the second one.
More concisely: For any additive group `G` and elements `a`, `b`, `c` in `G`, if `a + c = b`, then `a = b - c`.
|