inv_eq_one_divp'
theorem inv_eq_one_divp' : ∀ {α : Type u} [inst : Monoid α] (u : αˣ), ↑(1 / u) = 1 /ₚ u
The theorem `inv_eq_one_divp'` is used for a function called `field_simp` to handle the inverses of units. In a monoid structure of a type `α`, for any unit `u` of `α`, it states that the reciprocal of the unit `u` is equal to the p-adic inverse of `u`, essentially re-writing `↑u⁻¹ = ↑(1 / u)` as `↑(1 / u) = 1 /ₚ u`. In this context, `field_simp` prefers to use `inv_eq_one_div` to perform such rewrite.
More concisely: In a monoid with units, the reciprocal of a unit is equal to its p-adic inverse.
|
AddUnits.add_neg_cancel_left
theorem AddUnits.add_neg_cancel_left :
∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α) (b : α), ↑a + (↑(-a) + b) = b
The theorem `AddUnits.add_neg_cancel_left` states that for any type `α` which has an additive monoid structure and any element `a` of the additive units of `α` and `b` of type `α`, adding `a` and the negation of `a` to `b` results in `b`. In other words, the additive unit `a` and its negation `(-a)` cancel each other out when added to any `b`, in the context of an additive monoid.
More concisely: For any additive monoid type `α` and additive unit `a` in `α`, we have `a + (-a) = 0`, where `0` is the additive identity of `α`.
|
IsUnit.unit_spec
theorem IsUnit.unit_spec : ∀ {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a), ↑h.unit = a
This theorem, `IsUnit.unit_spec`, states that for any type `M` that has a `Monoid` instance and for any element `a` of `M` that is a unit (i.e., it has a two-sided inverse), the element of the group of units corresponding to `a` (obtained through the `IsUnit.unit` function) is equal to `a` when the function is applied to the proof that `a` is a unit. In other words, it ensures that the `IsUnit.unit` function correctly identifies the monoid unit element associated with a given unit element in the monoid `M`.
More concisely: For any type `M` with a `Monoid` instance and any unit `a` in `M`, `IsUnit.unit a` equals `a`.
|
isUnit_one
theorem isUnit_one : ∀ {M : Type u_1} [inst : Monoid M], IsUnit 1
This theorem states that for any type `M` that has a `Monoid` structure, the element `1` (which is the identity element in the monoid) is a unit. In other words, there exists an element in `M` that serves as a two-sided inverse for `1`. As per the monoid structure, this inverse is also `1` itself. Therefore, within any monoid, the identity element is considered a unit.
More concisely: For any Monoid M, the identity element 1 is a unit with left and right inverse equal to 1.
|
AddUnits.add_neg_cancel_right
theorem AddUnits.add_neg_cancel_right :
∀ {α : Type u} [inst : AddMonoid α] (a : α) (b : AddUnits α), a + ↑b + ↑(-b) = a
This theorem states that for any type `α` that has an additive monoid structure, and any elements `a` of type `α` and `b` of type `AddUnits α` (which means `b` is an additive unit in `α`), adding `b` and the additive inverse of `b` to `a` (in that order) will just result in `a`. In mathematical terms, it's saying that for all `a` in `α` and `b` in `AddUnits α`, `a + b + (-b) = a`. This is a formal statement of the property that adding an element and its additive inverse results in no change.
More concisely: For any additive monoid type `α` and its additive unit `b`, the equation `a + b + (-b) = a` holds for all `a` in `α`.
|
Units.mul_left_inj
theorem Units.mul_left_inj : ∀ {α : Type u} [inst : Monoid α] (a : αˣ) {b c : α}, b * ↑a = c * ↑a ↔ b = c
This theorem, `Units.mul_left_inj`, states that for any type `α` that forms a monoid, given a unit `a` of `α` and any two elements `b` and `c` of `α`, the equality `b * a = c * a` holds if and only if `b = c`. In other words, multiplying a monoid element by a unit on the right side is an injective operation, meaning it preserves distinctness. If the products of `b` and `c` with `a` are equal, then `b` and `c` must have been equal to begin with.
More concisely: For any monoid type `α` and unit `a` in `α`, the multiplication by `a` on the right is an injection: `(x : α) → x * a = y * a ↔ x = y`.
|
Mathlib.Algebra.Group.Units._auxLemma.31
theorem Mathlib.Algebra.Group.Units._auxLemma.31 : ∀ {M : Type u_1} [inst : Monoid M], IsUnit 1 = True
This theorem states that for any type `M` that has a `Monoid` structure, the multiplicative identity element `1` is a unit. This means that `1` has a two-sided inverse in the `Monoid` `M`. In other words, there exists an element in `M` which when multiplied with `1` gives `1` again. This holds true for any `Monoid` structure.
More concisely: For any type `M` equipped with a `Monoid` structure, the multiplicative identity `1` is a unit with a two-sided inverse in `M`.
|
AddUnits.ext
theorem AddUnits.ext : ∀ {α : Type u} [inst : AddMonoid α], Function.Injective AddUnits.val
The theorem `AddUnits.ext` states that for any type `α` which forms an additive monoid, the function `AddUnits.val` is injective. In other words, if `α` is a type with an additive monoid structure, and we have two elements of the type `AddUnits α` that map to the same element in `α` under the `AddUnits.val` function, they must have been the same element in `AddUnits α` to begin with.
More concisely: If `α` is an additive monoid, then the function `AddUnits.val` from `AddUnits α` to `α` is an injection.
|
AddUnits.val_neg_eq_neg_val
theorem AddUnits.val_neg_eq_neg_val : ∀ {α : Type u} [inst : SubtractionMonoid α] (u : AddUnits α), ↑(-u) = -↑u := by
sorry
This theorem states that for any type `α` that forms a `SubtractionMonoid` (a structure with addition, zero, and subtraction operations satisfying certain properties), given an additive unit `u` of `α`, the value of the negation of `u` is equal to the negation of the value of `u`. In more mathematical terms, it says if `u` is an additive unit in `α`, then `-(u)` equals `-u`, where the notation `-` denotes negation.
More concisely: For any additive unit `u` in a type `α` forming a `SubtractionMonoid`, we have `-(u) = -u`.
|
val_div_eq_divp
theorem val_div_eq_divp : ∀ {α : Type u} [inst : Monoid α] (u₁ u₂ : αˣ), ↑(u₁ / u₂) = ↑u₁ /ₚ u₂
This theorem, `val_div_eq_divp`, states that for any type `α` that forms a monoid, and for any two units `u₁` and `u₂` of this type, the division of `u₁` and `u₂` (which results in another unit) when coerced to the underlying type `α`, is equal to the division of `u₁` and `u₂` in `α`. Here, `u₁ /ₚ u₂` denotes the division of `u₁` and `u₂` in `α`, where `u₁` and `u₂` are units of `α`. Essentially, it says that the operation of division behaves the same way in the unit group as it does in the underlying monoid.
More concisely: For any monoid type `α` with units `u₁` and `u₂`, `u₁ / u₂ = u₁⁻¹ * u₂⁻¹ /ₚ u₁ * u₂`, where `/ₚ` denotes division in `α` and `*` denotes multiplication in `α`, and `u₁⁻¹` and `u₂⁻¹` are the multiplicative inverses of `u₁` and `u₂` in the multiplicative monoid of `α`.
|
Mathlib.Algebra.Group.Units._auxLemma.27
theorem Mathlib.Algebra.Group.Units._auxLemma.27 :
∀ {M : Type u_1} [inst : Monoid M] [inst_1 : Subsingleton M] (a : M), IsUnit a = True
The theorem `Mathlib.Algebra.Group.Units._auxLemma.27` states that for any type `M` that is a Monoid (a mathematical structure with a binary operation that is associative, and an identity element), and further assuming `M` is a Subsingleton (i.e., it has at most one distinct element), then any element `a` of `M` is a unit. In other words, every element `a` of such a Monoid `M` has a two-sided inverse. Here the two-sided inverse is defined in a bundled form, where an element `a` is a unit if there exists some `u` such that `u` when coerced (`↑u`) equals `a`.
More concisely: In a Monoid of at most one element, every element is a unit with a two-sided inverse.
|
Mathlib.Algebra.Group.Units._auxLemma.29
theorem Mathlib.Algebra.Group.Units._auxLemma.29 : ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ), IsUnit ↑u = True := by
sorry
This theorem states that for any type `M` that forms a Monoid, an element `u` of the group of units `Mˣ` is always a unit. In other words, every element in the group of units `Mˣ` has a two-sided inverse in the Monoid `M`. This is a property of Monoids that underscores the relationship between the group of units and the concept of unit elements.
More concisely: Every unit in a monoid is an element of the monoid's group of units, and possesses a two-sided inverse in the monoid.
|
one_divp
theorem one_divp : ∀ {α : Type u} [inst : Monoid α] (u : αˣ), 1 /ₚ u = ↑u⁻¹
This theorem, named `one_divp`, states that for any type `α` that forms a Monoid (a kind of algebraic structure), and any non-zero element `u` of type `α`, the value of 1 divided by `u` (expressed as `1 /ₚ u`) is equal to the inverse of `u` (expressed as `↑u⁻¹`). In terms of algebra, it's stating that division by an element in a Monoid is equivalent to multiplying by its inverse.
More concisely: For any Monoid type `α` and non-zero element `u` of `α`, `1 /ₚ u = ↑u⁻¹`. That is, division by `u` equals the multiplicative inverse of `u`.
|
AddUnits.neg_val
theorem AddUnits.neg_val : ∀ {α : Type u} [inst : AddMonoid α] (self : AddUnits α), self.neg + ↑self = 0
This theorem, `AddUnits.neg_val`, states that for any type `α` that is an instance of `AddMonoid`, the negation (`neg`) of any value (`self`) in `AddUnits α` when added to the original value (`self`) equals zero. In other words, this theorem indicates that the `neg` operation acts as the left additive inverse in the base `AddMonoid` structure. This is similar to how the negative of a number is its additive inverse in standard arithmetic.
More concisely: For all `α` an instance of `AddMonoid`, `neg (self : AddUnits α) + self = 0`.
|
IsAddUnit.add
theorem IsAddUnit.add :
∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, IsAddUnit a → IsAddUnit b → IsAddUnit (a + b)
The theorem `IsAddUnit.add` states that for any type `M` that is an instance of `AddMonoid`, if `a` and `b` are elements of `M` and both `a` and `b` are `AddUnit` elements (i.e., they have a two-sided additive inverse), then the sum of `a` and `b` is also an `AddUnit`. In other words, the sum of two elements, each having a two-sided additive inverse, also has a two-sided additive inverse.
More concisely: If `a` and `b` are elements of an additive monoid `M` with two-sided additive inverses, then `a + b` also has a two-sided additive inverse.
|
IsUnit.inv
theorem IsUnit.inv : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α}, IsUnit a → IsUnit a⁻¹
The theorem `IsUnit.inv` states that for any type `α` that is a division monoid, for any element `a` of `α`, if `a` is a unit (i.e., it has a two-sided inverse), then the inverse of `a` (`a⁻¹`) is also a unit. In other words, if an element has an inverse in the division monoid, then its inverse also has an inverse, which is the original element itself.
More concisely: If `α` is a division monoid and `a` is a unit in `α`, then `a⁻¹` is also a unit in `α`.
|
Units.isUnit_units_mul
theorem Units.isUnit_units_mul : ∀ {M : Type u_3} [inst : Monoid M] (u : Mˣ) (a : M), IsUnit (↑u * a) ↔ IsUnit a := by
sorry
The theorem `Units.isUnit_units_mul` states that for all elements `a` from any Monoid `M`, and for all unit elements `u` in `M`, the property of being a unit is preserved under left multiplication by `u`. In other words, `a` is a unit if and only if the product of `u` and `a` is a unit. This is true in the context of a mathematical structure called a Monoid, where a unit element is one that has a two-sided inverse.
More concisely: For all units `u` in a monoid `M` and all elements `a` in `M`, `a` is a unit if and only if `u * a` and `a * u` are units.
|
IsAddUnit.add_right_inj
theorem IsAddUnit.add_right_inj :
∀ {M : Type u_1} [inst : AddMonoid M] {a b c : M}, IsAddUnit a → (a + b = a + c ↔ b = c)
The theorem `IsAddUnit.add_right_inj` states that for any type `M` that is an additive monoid (`AddMonoid M`), and for any elements `a`, `b`, and `c` in `M`, if `a` is an additive unit (i.e., it has a two-sided additive inverse), then the equality of `a + b` and `a + c` implies the equality of `b` and `c`. In essence, this theorem guarantees the cancelability of the additive unit from the left side of an equation in an additive monoid.
More concisely: If `a` is an additive unit in an additive monoid `M`, then `a + b = a + c` implies `b = c`.
|
IsUnit.mul_right_inj
theorem IsUnit.mul_right_inj : ∀ {M : Type u_1} [inst : Monoid M] {a b c : M}, IsUnit a → (a * b = a * c ↔ b = c) := by
sorry
The theorem `IsUnit.mul_right_inj` states that for any monoid `M`, and any elements `a`, `b`, and `c` of `M`, if `a` is a unit (i.e., it has a two-sided inverse), then the equality `a * b = a * c` implies `b = c`. In other words, for a unit `a` in a monoid, multiplication by `a` is injective on the right.
More concisely: If `a` is a unit in a monoid `M`, then `a * b = a * c` implies `b = c`.
|
Units.inv_mul_cancel_left
theorem Units.inv_mul_cancel_left : ∀ {α : Type u} [inst : Monoid α] (a : αˣ) (b : α), ↑a⁻¹ * (↑a * b) = b
This theorem states that for any type `α` that forms a Monoid (a mathematical structure with an associative binary operation and an identity element), given an invertible element `a` (denoted as `a : αˣ`) and any other element `b`, multiplying `b` by `a` and then by the inverse of `a` (from the left) will give back the original `b`. In other words, the left multiplication by an invertible element and its inverse in a Monoid is a canceling operation, which is analogous to multiplying by one in basic arithmetic. This principle is written in mathematical notation as: `a⁻¹ * (a * b) = b`.
More concisely: For any Monoid `α` and invertible element `a : αˣ`, `a⁻¹ * (a * b) = b`.
|
AddUnits.isAddUnit_add_addUnits
theorem AddUnits.isAddUnit_add_addUnits :
∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (u : AddUnits M), IsAddUnit (a + ↑u) ↔ IsAddUnit a
The theorem `AddUnits.isAddUnit_add_addUnits` states that for any type `M` that has an `AddMonoid` structure, and for any element `a` of `M` and `u` of `AddUnits M`, the property of `a` being an `AddUnit` is unchanged when `u` is added to `a`. In other words, an element `a` is an `AddUnit` if and only if `a + u` is an `AddUnit`, where `u` is an `AddUnit` of `M`. This underscores the characteristic of `AddUnits` serving as two-sided additive inverses in the `AddMonoid` structure.
More concisely: For any `AddMonoid` type `M` and its `AddUnit` `u`, if `a` is an `AddUnit` of `M`, then `a + u` is also an `AddUnit` of `M`.
|
isUnit_of_mul_eq_one
theorem isUnit_of_mul_eq_one : ∀ {M : Type u_1} [inst : CommMonoid M] (a b : M), a * b = 1 → IsUnit a
This theorem states that for any type `M` that is a commutative monoid, if we have two elements `a` and `b` of `M` such that the product of `a` and `b` equals the identity element `1`, then `a` is a unit in `M`. In the context of mathematics, a unit is an element in a ring (or in this case, monoid) that has a multiplicative inverse. Therefore, this theorem is essentially saying that if two elements multiply to give the identity, then each of those elements must have a multiplicative inverse, i.e., they are units.
More concisely: In a commutative monoid, if an element has an identity product with another element, then it is a unit.
|
Units.inv_val
theorem Units.inv_val : ∀ {α : Type u} [inst : Monoid α] (self : αˣ), self.inv * ↑self = 1
This theorem states that for any type `α` which forms a Monoid, the `inv` function acts as the left inverse of the `val` function. Specifically, if we take any element `self` from the group of units `αˣ` (nonzero elements under multiplication in `α`), then multiplying `inv` of `self` with the coercion of `self` (`↑self`, reading the element of `αˣ` as an element of `α`) always results in the identity element of the Monoid (`1`). This property is fundamental to the structure of a monoid with inverses (a group).
More concisely: For any monoid `α` with units, the function `inv` acting on units is the left inverse of the coercion function, i.e., `inv (↑a) * a = 1` for all units `a` in `α`.
|
inv_eq_one_divp
theorem inv_eq_one_divp : ∀ {α : Type u} [inst : Monoid α] (u : αˣ), ↑u⁻¹ = 1 /ₚ u
This theorem, `inv_eq_one_divp`, states that for any given type `α` that is a monoid (a set equipped with an associative binary operation that has an identity element), the inverse of any unit `u` in `α` is equal to one divided by `u`. The notation `1 /ₚ u` represents the division of 1 by `u` in the case where `u` is a unit in the monoid. This theorem is used for `field_simp` to handle inverses of units.
More concisely: For any monoid `α` and unit `u` in `α`, the inverse of `u` is equal to the multiplicative inverse of `1` with respect to `u`, i.e., `u⁻¹ = 1 /ₚ u`.
|
IsUnit.pow
theorem IsUnit.pow : ∀ {M : Type u_1} [inst : Monoid M] {a : M} (n : ℕ), IsUnit a → IsUnit (a ^ n)
This theorem states that for any type `M` equipped with a monoid structure, if an element `a` of `M` is a unit (meaning that it has a two-sided inverse), then `a` raised to any natural number `n` (denoted as `a ^ n`) is also a unit. Essentially, it asserts that the power of a unit in a monoid is still a unit.
More concisely: If `M` is a monoid and `a` is a unit in `M`, then for all natural numbers `n`, `a^n` is also a unit in `M`.
|
Units.isUnit_mul_units
theorem Units.isUnit_mul_units : ∀ {M : Type u_1} [inst : Monoid M] (a : M) (u : Mˣ), IsUnit (a * ↑u) ↔ IsUnit a := by
sorry
This theorem states that for any type `M` that forms a monoid, given an element `a` from `M` and a unit `u` from `Mˣ`, the condition of `a` being a unit (i.e., `a` having a two-sided inverse) is unaffected by right multiplication with the unit `u`. In other words, `a` is a unit if and only if `a * u` is a unit.
More concisely: For any monoid `M` and its unit `u`, an element `a` in `M` is a unit if and only if `a` and `a * u` are mutual inverses.
|
Units.val_inv_eq_inv_val
theorem Units.val_inv_eq_inv_val : ∀ {α : Type u} [inst : DivisionMonoid α] (u : αˣ), ↑u⁻¹ = (↑u)⁻¹
This theorem states that, for all types `α` that are division monoids, the inverse of the unit `u` in `α` is the same as the inverse of the value of `u`. More formally, for every `u` in the units of `α`, the embedding of the inverse of `u` (`↑u⁻¹`) equals the inverse of the embedding of `u` (`(↑u)⁻¹`). Essentially, this means that the operation of taking the inverse commutes with the operation of taking the value of a unit in a division monoid.
More concisely: For all division monoids `α` and units `u` in `α`, the inverse of `u` equals the inverse of its embedding, i.e., `↑u⁻¹ = (↑u)⁻¹`.
|
isUnit_iff_exists_inv
theorem isUnit_iff_exists_inv : ∀ {M : Type u_1} [inst : CommMonoid M] {a : M}, IsUnit a ↔ ∃ b, a * b = 1
This theorem states that, for any commutative monoid M and any element 'a' of M, 'a' is a unit if and only if there exists another element 'b' in M such that the product of 'a' and 'b' equals the identity element of M. In other words, 'a' is a unit precisely when it has a multiplicative inverse.
More concisely: A commutative monoid element 'a' is a unit if and only if there exists an element 'b' such that 'a' * 'b' = id\_M, where id\_M is the identity element of M.
|
AddUnits.neg_add_eq_iff_eq_add
theorem AddUnits.neg_add_eq_iff_eq_add :
∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α) {b c : α}, ↑(-a) + b = c ↔ b = ↑a + c
This theorem states that for any given type `α` with an additive monoid structure, and given an additive unit `a` and two elements `b` and `c` of the type `α`, the negative of `a` added to `b` equals `c` if and only if `b` equals the additive unit `a` added to `c`. In mathematical terms, it's saying that if `-a + b = c`, then `b = a + c`, and vice versa, within the context of an additive monoid.
More concisely: For any additive monoid type `α` with additive unit `a`, the elements `b` and `c` satisfy `-a + b = c` if and only if `b = a + c`.
|
isUnit_of_mul_isUnit_right
theorem isUnit_of_mul_isUnit_right : ∀ {M : Type u_1} [inst : CommMonoid M] {x y : M}, IsUnit (x * y) → IsUnit y := by
sorry
This theorem states that for any type `M` that is a commutative monoid (which implies that the operation of the monoid is commutative), if an element `y` of `M` is such that the product of `y` and any other element `x` in `M` is a unit (i.e., it has a two-sided inverse), then `y` itself must also be a unit. In other words, if the product of `x` and `y` is an element that possesses an inverse, then `y` must also possess an inverse.
More concisely: If `M` is a commutative monoid and `y` in `M` has a two-sided inverse for every `x` in `M`, then `y` is a unit in `M`.
|
IsAddUnit.sub_add_left
theorem IsAddUnit.sub_add_left :
∀ {α : Type u} [inst : SubtractionMonoid α] {a b : α}, IsAddUnit b → b - (a + b) = 0 - a
This theorem states that for any type `α` which forms a `SubtractionMonoid`, and any elements `a` and `b` of type `α`, if `b` is an `AddUnit` (meaning it has a two-sided additive inverse), then subtracting `a + b` from `b` results in the same value as subtracting `a` from `0`. In mathematical terms, if `b` is an element of an additive monoid that possesses a two-sided additive inverse, then `b - (a + b)` is equal to `0 - a`.
More concisely: For any `α` that is a SubtractionMonoid and has an AddUnit `b`, we have `b - (a + b) = 0 - a`, where `a` is an element of `α`.
|
divp_mul_eq_mul_divp
theorem divp_mul_eq_mul_divp : ∀ {α : Type u} [inst : CommMonoid α] (x y : α) (u : αˣ), x /ₚ u * y = x * y /ₚ u := by
sorry
This theorem, `divp_mul_eq_mul_divp`, states that for any type `α` that is a commutative monoid (i.e., a mathematical structure with a binary operation that is associative, has an identity element, and is commutative), given any two elements `x` and `y` of `α` and a unit `u` of `α`, the operation of dividing `x` by `u` (`x /ₚ u`) and then multiplying by `y` is equivalent to the operation of multiplying `x` and `y` first and then dividing by `u` (`x * y /ₚ u`). Essentially, it's stating a property of distributivity of division over multiplication in a commutative monoid.
More concisely: For any commutative monoid `α` and elements `x`, `y`, and unit `u` in `α`, `x /ₚ u * y = x * y /ₚ u`.
|
IsUnit.mul_inv_cancel
theorem IsUnit.mul_inv_cancel : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α}, IsUnit a → a * a⁻¹ = 1
This theorem states that for any type `α` that forms a division monoid, given an element `a` of type `α` that is a unit, the product of `a` and its inverse `a⁻¹` equals 1. In mathematical terms, this theorem is expressing that if `a` is a unit in a division monoid (meaning it has a multiplicative inverse), then multiplying `a` by its inverse will yield the multiplicative identity, often denoted as 1. This is a fundamental property of elements with multiplicative inverses in algebraic structures, such as groups and monoids.
More concisely: In a division monoid, the product of any unit `a` and its multiplicative inverse `a⁻¹` equals the multiplicative identity 1.
|
Units.val_one
theorem Units.val_one : ∀ {α : Type u} [inst : Monoid α], ↑1 = 1
This theorem states that for any type `α` that forms a monoid, the value of the "lifting" or "upcasting" of 1 (i.e., `↑1`) is equal to 1. Here, `Units.val_one` means that the monoid unit (which is usually denoted as `1` in abstract algebra) remains unchanged when it is cast from the set of units (`Units`) to the underlying monoid (`α`).
More concisely: For any monoid type `α`, the upcasting of its unit `1` (denoted `↑1`) is equal to the monoid unit itself (`Units.val_one`).
|
Units.inv_eq_of_mul_eq_one_right
theorem Units.inv_eq_of_mul_eq_one_right : ∀ {α : Type u} [inst : Monoid α] {u : αˣ} {a : α}, ↑u * a = 1 → ↑u⁻¹ = a
This theorem states that for any type `α` that forms a monoid, and for any unit `u` and element `a` of this type, if the product of `u` and `a` equals 1 (the multiplicative identity of the monoid), then the inverse of `u` is equal to `a`. In mathematical terms, `u * a = 1` implies `u⁻¹ = a` for all `u` and `a` in a given monoid `α`.
More concisely: If `u` is the multiplicative identity of a monoid `α` with invertible element `a`, then `u = a⁻¹`.
|
Group.isUnit
theorem Group.isUnit : ∀ {α : Type u} [inst : Group α] (a : α), IsUnit a
This theorem states that for any type `α` that forms a group (denoted by `[inst : Group α]`), every element `a` of type `α` is a unit. In mathematical terms, this states that every element of a group has a two-sided inverse, meaning for any element `a` in a group there exists an element `u` such that the multiplication of `a` and `u` (in either order) equals the identity element of the group. This property holds for all groups and is one of the defining characteristics of a group in algebra.
More concisely: Every element in a group has a two-sided inverse.
|
Units.val_mul
theorem Units.val_mul : ∀ {α : Type u} [inst : Monoid α] (a b : αˣ), ↑(a * b) = ↑a * ↑b
This theorem states that for any given type `α` that forms a Monoid, the multiplication of two elements `a` and `b` from the group of units of `α` (denoted as `αˣ`), when coerced to `α`, is equal to the product of `a` and `b` individually coerced to `α`. In other words, the coercion operation preserves the multiplication operation from the group of units to the monoid.
More concisely: For any monoid `α` and units `a, b` in `αˣ`, the coercion of `a * b` from `αˣ` to `α` is equal to the coercion of `a` and `b` individually from `αˣ` to `α` multiplied in `α`.
|
Units.mul_inv_cancel_left
theorem Units.mul_inv_cancel_left : ∀ {α : Type u} [inst : Monoid α] (a : αˣ) (b : α), ↑a * (↑a⁻¹ * b) = b
This theorem states that for any type `α` that is a Monoid, and for any units `a` and any element `b` of that Monoid, the product of `a` and the product of the inverse of `a` and `b` equals `b`. In mathematical terms, it states that `a * (a⁻¹ * b) = b`. This is a property of Monoids, where the multiplication of any element and its inverse results in the identity element, effectively 'canceling out' the original element.
More concisely: For any monoid `α` and elements `a` with invertible `a⁻¹` in `α`, `a * (a⁻¹ * b) = b`.
|
Units.inv_mul_eq_iff_eq_mul
theorem Units.inv_mul_eq_iff_eq_mul : ∀ {α : Type u} [inst : Monoid α] (a : αˣ) {b c : α}, ↑a⁻¹ * b = c ↔ b = ↑a * c
This theorem states that for any type `α` that forms a monoid, and given a unit `a` of type `α` and two elements `b` and `c` of type `α`, the equation `a⁻¹ * b = c` is true if and only if `b = a * c`. Here, `a⁻¹` denotes the inverse of unit `a`. Both `aˣ` and `α` belong to the same monoid and the inverse of a unit is also a unit in the monoid.
More concisely: For any monoid `α` with unit `a`, `a⁻¹ * b = c` if and only if `b = a * c`.
|
IsUnit.div_mul_cancel
theorem IsUnit.div_mul_cancel : ∀ {α : Type u} [inst : DivisionMonoid α] {b : α}, IsUnit b → ∀ (a : α), a / b * b = a
The theorem `IsUnit.div_mul_cancel` states that for any type `α` that forms a Division Monoid, and for any element `b` of type `α` that is a unit (i.e., has a two-sided inverse), for any element `a` of type `α`, the operation of dividing `a` by `b`, and then multiplying the result by `b`, gives us back the original element `a`. In other words, if `b` is a unit in a division monoid, division by `b` followed by multiplication by `b` is a cancelling operation.
More concisely: For any division monoid `α` and unit `b` in `α`, we have `(a / b) * b = a` for all `a` in `α`.
|
Units.eq_iff
theorem Units.eq_iff : ∀ {α : Type u} [inst : Monoid α] {a b : αˣ}, ↑a = ↑b ↔ a = b
This theorem states that for all types `α` which possess a Monoid structure, two units `a` and `b` of type `α` are equal if and only if their canonical embeddings into `α` are equal. In other words, it provides a condition for the equality of two elements of the group of units of a monoid, using the equality of their representations in the monoid structure itself.
In mathematical terms, we're basically saying if a and b are elements of the unit group of a monoid, then a equals b if and only if their embeddings in the monoid are equal.
More concisely: For all types `α` with a Monoid structure and units `a` and `b` in `α`, `a = b` if and only if their monoid embeddings `[a : α] = [b : α]` hold.
|
IsUnit.div_eq_iff
theorem IsUnit.div_eq_iff : ∀ {α : Type u} [inst : DivisionMonoid α] {a b c : α}, IsUnit b → (a / b = c ↔ a = c * b)
This theorem states that for any type `α` that is a division monoid, and any elements `a`, `b`, and `c` in `α`, if `b` is a unit (i.e., it has a two-sided inverse), then the condition of `a` divided by `b` being equal to `c` is equivalent to the condition of `a` being equal to `c` multiplied by `b`. In other words, it provides a way to rewrite division as multiplication in the presence of a unit element.
More concisely: For any division monoid `α` and units `b` in `α`, the condition `a / b = c` is equivalent to `a = c * b`.
|
Units.val_eq_one
theorem Units.val_eq_one : ∀ {α : Type u} [inst : Monoid α] {a : αˣ}, ↑a = 1 ↔ a = 1
This theorem, named `Units.val_eq_one`, states that for any type `α` that has a monoid structure, and for any unit `a` of `α`, the value of `a` is equal to 1 if and only if `a` itself is equal to 1. In other words, in the context of a monoid, a unit `a` has a value of 1 exactly when `a` is the unit of the monoid.
More concisely: For any monoid `α` and unit `a` in `α`, `a` equals 1 if and only if `a` is the identity element of the monoid.
|
AddUnits.isAddUnit
theorem AddUnits.isAddUnit : ∀ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M), IsAddUnit ↑u
This theorem states that for any `AddUnits M` in an additive monoid `M`, the element `u` is an `AddUnit`. In other words, every element `u` of the type `AddUnits M` is such that there exists an element in the same monoid that when added to `u` gives the additive identity of the monoid. This implies that every `u` in `AddUnits M` has a two-sided additive inverse.
More concisely: Every element in the type of additive units of an additive monoid has a two-sided additive inverse.
|
AddUnits.neg_add_cancel_right
theorem AddUnits.neg_add_cancel_right :
∀ {α : Type u} [inst : AddMonoid α] (a : α) (b : AddUnits α), a + ↑(-b) + ↑b = a
This theorem, `AddUnits.neg_add_cancel_right`, states that for any type `α` that forms an additive monoid, and for any elements `a` of type `α` and `b` of type `AddUnits α` (which is a type of additive units), adding `a` to the additive inverse of `b` (represented by `-b`) and then adding `b` results in `a`. In the language of mathematics, this can be expressed as \(a + (-b) + b = a\). Essentially, it's stating that the "additive cancellation" property holds in this monoid.
More concisely: For any additive monoid type `α` and its additive unit `b`, we have `a + (-b) = a` for all `a` in `α`.
|
IsUnit.mul_left_inj
theorem IsUnit.mul_left_inj : ∀ {M : Type u_1} [inst : Monoid M] {a b c : M}, IsUnit a → (b * a = c * a ↔ b = c) := by
sorry
The theorem `IsUnit.mul_left_inj` states that for any type `M` that has a `Monoid` structure, and for any elements `a`, `b`, and `c` of `M`, if `a` is a unit (i.e., it has a two-sided inverse), then the equality `b * a = c * a` implies `b = c`. In other words, left multiplication by a unit element in a monoid is injective.
More concisely: If `a` is a unit in a monoid `M`, then the map left multiplication by `a` is injective: `∀ (b c : M), b * a = c * a → b = c`.
|
Units.mul_inv
theorem Units.mul_inv : ∀ {α : Type u} [inst : Monoid α] (a : αˣ), ↑a * ↑a⁻¹ = 1
This theorem states that for any type `α` that forms a Monoid (a set equipped with an associative binary operation and an identity element), the multiplication of any unit `a` and its inverse yields the identity element. In mathematical terms, for any `a` in the group of units of `α`, `a * a⁻¹ = 1`. This is a fundamental property of elements in any Monoid.
More concisely: For any monoid `α` and its unit `a`, `a * a⁻¹ = 1`.
|
Units.inv_mul_cancel_right
theorem Units.inv_mul_cancel_right : ∀ {α : Type u} [inst : Monoid α] (a : α) (b : αˣ), a * ↑b⁻¹ * ↑b = a
This theorem states that for any type `α` that forms a monoid (a structure where we have an associative binary operation, and an identity element relative to this operation), if you take any element `a` of type `α` and another element `b` which is a unit (meaning it has a multiplicative inverse), then multiplying `a` by the inverse of `b` and then by `b` itself will just give you `a` back. This effectively expresses the property that multiplying by a unit's inverse and the unit itself is a form of cancellation, returning you to your original value of `a`.
More concisely: For any monoid `α` and elements `a` of type `α` with a unit `b`, `a * b ^-1 * b = a`, where `*` denotes the monoid operation and `^-1` denotes the multiplicative inverse.
|
IsUnit.div_self
theorem IsUnit.div_self : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α}, IsUnit a → a / a = 1
The theorem `IsUnit.div_self` states that for any type `α`, which is a division monoid (a type of monoid with a division operation), and for any element `a : α`, if `a` is a unit (i.e., it has a two-sided inverse), then dividing `a` by itself yields 1. This property is a common one in mathematical structures with division, where any non-zero element divided by itself equals the multiplicative identity, which is 1 in this case.
More concisely: If `α` is a division monoid and `a : α` is a unit, then `a * (a ^ -1) = a ^ -1 * a = 1`, where `*` denotes division and `^` denotes exponentiation.
|
IsUnit.mul_iff
theorem IsUnit.mul_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {x y : M}, IsUnit (x * y) ↔ IsUnit x ∧ IsUnit y := by
sorry
This theorem, `IsUnit.mul_iff`, states that for any commutative monoid `M` and any elements `x` and `y` of `M`, the statement that the product of `x` and `y` is a unit is equivalent to the conjunction of the statements that `x` is a unit and `y` is a unit. In simpler terms, it says that in a commutative monoid, a product is a unit if and only if both factors are units.
More concisely: In a commutative monoid, the product of two elements is a unit if and only if both elements are units.
|
Units.val_inv
theorem Units.val_inv : ∀ {α : Type u} [inst : Monoid α] (self : αˣ), ↑self * self.inv = 1
The theorem `Units.val_inv` states that for any type α that forms a monoid, the multiplicative inverse `inv` is the right inverse of the value `val` for any unit `self` of this monoid. In other words, when you multiply a unit `self` by its multiplicative inverse, you get the multiplicative identity of the monoid, which is 1.
More concisely: For any monoid type α and unit self of α, self * inv self = 1, where inv is the multiplicative inverse of self.
|
Units.inv_mul_eq_one
theorem Units.inv_mul_eq_one : ∀ {α : Type u} [inst : Monoid α] {u : αˣ} {a : α}, ↑u⁻¹ * a = 1 ↔ ↑u = a
This theorem states that for any type `α` that forms a Monoid (a set equipped with an associative binary operation and an identity element) and any element `u` of the multiplicative group of non-zero elements of `α` represented as `αˣ`, and for any `a` belonging to `α`, the product of the inverse of `u` and `a` equals the identity element (1 in this case) if and only if `u` equals `a`. This is a property of units in a Monoid.
More concisely: For any monoid `α` and its multiplicative group `αˣ`, if `u` is a unit in `α` and `a` is an element of `α` such that `u * a = 1` in `αˣ`, then `u = a`.
|
IsUnit.eq_div_iff
theorem IsUnit.eq_div_iff : ∀ {α : Type u} [inst : DivisionMonoid α] {a b c : α}, IsUnit c → (a = b / c ↔ a * c = b)
This theorem, `IsUnit.eq_div_iff`, states that for any division monoid `α` and any elements `a`, `b`, and `c` of `α`, if `c` is a unit (meaning `c` has a two-sided inverse), then `a` is equal to `b` divided by `c` if and only if `a` multiplied by `c` is equal to `b`. In other words, in the context of a division monoid, division and multiplication by a unit element are interchangeable operations.
More concisely: In a division monoid, for all `a`, `b`, and `c` (with `c` being a unit), `a = b / c` if and only if `a * c = b`.
|
AddUnits.neg_add
theorem AddUnits.neg_add : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α), ↑(-a) + ↑a = 0
This theorem, `AddUnits.neg_add`, states that for any type `α` that is an additive monoid, and for any additive unit `a` of this type, the sum of the negative of `a` and `a` itself is always equal to zero. It mirrors the familiar property of numbers that the addition of a number and its negative yields zero.
More concisely: For any additive monoid type `α` and additive unit `a`, `-a + a = 0`.
|
IsUnit.val_inv_mul
theorem IsUnit.val_inv_mul : ∀ {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a), ↑h.unit⁻¹ * a = 1
The theorem `IsUnit.val_inv_mul` states that for any type `M` that has a Monoid structure and any element `a` of `M` which is a unit (meaning it has a two-sided inverse), the inverse of the unit corresponding to `a` (given by `IsUnit.unit h`) times `a` equals the multiplicative identity `1`. In essence, it establishes that for a unit element in a monoid, multiplying it by its inverse results in the multiplicative identity.
More concisely: For any monoid `M` and unit `a` in `M`, `IsUnit.unit h * a = 1` where `IsUnit.unit h` is the inverse of `a`.
|
IsAddUnit.sub_add_cancel
theorem IsAddUnit.sub_add_cancel :
∀ {α : Type u} [inst : SubtractionMonoid α] {b : α}, IsAddUnit b → ∀ (a : α), a - b + b = a
This theorem states that for any type `α` that forms a subtraction monoid, if an element `b` of `α` is an additive unit (meaning it has a two-sided additive inverse), then for any element `a` of `α`, the operation of subtracting `b` from `a`, then adding `b` back to the result, is the same as doing nothing to `a` (i.e., `a - b + b` equals `a`).
In other words, it formalizes the intuitive property of subtraction and addition where the subtracted quantity `b` can be added back to restore the original value `a`. The specific condition that `b` is an additive unit ensures that the addition operation is well-defined and invertible.
More concisely: For any type `α` that forms a subtraction monoid with additive unit `b`, we have `a - b + b = a` for all `a` in `α`.
|
IsUnit.mul
theorem IsUnit.mul : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, IsUnit a → IsUnit b → IsUnit (a * b)
This theorem states that for any type `M` with a `Monoid` structure and any two elements `a` and `b` of `M`, if `a` and `b` are both units (i.e., each has a two-sided inverse), then their product `a * b` is also a unit. In other words, the product of two invertible elements in a monoid is itself invertible.
More concisely: If `M` is a monoid and `a` and `b` are invertible elements of `M`, then `a * b` is an invertible element of `M`.
|
IsUnit.exists_right_inv
theorem IsUnit.exists_right_inv : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, IsUnit a → ∃ b, a * b = 1
This theorem, `IsUnit.exists_right_inv`, states that for any given type `M` that is a Monoid, and any element `a` of `M` that is a unit (i.e., it has a two-sided inverse), there exists another element `b` such that the product of `a` and `b` is the identity element of the Monoid, which is `1`. In other words, if `a` is a unit in a Monoid, it has a right inverse.
More concisely: Given a Monoid `M` and a unit `a` in `M`, there exists a right inverse `b` such that `a * b = 1`.
|
AddUnits.neg_eq_of_add_eq_zero_right
theorem AddUnits.neg_eq_of_add_eq_zero_right :
∀ {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α}, ↑u + a = 0 → ↑(-u) = a
This theorem states that for any type `α` equipped with an additive monoid structure, given an additive unit `u` and an element `a` from `α`, if the sum of the coercions of `u` and `a` equals zero, then the coercion of the additive inverse of `u` is equal to `a`. In other words, in the context of an additive monoid, if adding a certain element to another results in zero, the second element is the additive inverse of the first.
More concisely: For any additive monoid type `α` and its additive unit `u` with `u + a = 0` implying `a = -u`.
|
Units.isUnit
theorem Units.isUnit : ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ), IsUnit ↑u
The theorem `Units.isUnit` states that for any type `M` that forms a Monoid, any element `u` of `Mˣ` (the set of units in the monoid `M`) is a unit. In other words, if `u` is an element of the set of units in the monoid `M`, then there exists another element in the monoid such that the product of `u` and this element is the monoid's identity.
More concisely: For any monoid `M` and any of its unit element `u`, there exists an element `e` in `M` such that `u * e = e * u = 1_M`, where `1_M` is the identity element of `M`.
|
IsAddUnit.add_left_inj
theorem IsAddUnit.add_left_inj :
∀ {M : Type u_1} [inst : AddMonoid M] {a b c : M}, IsAddUnit a → (b + a = c + a ↔ b = c)
The theorem `IsAddUnit.add_left_inj` states that for any type `M` that has an additive monoid structure, and for any elements `a`, `b`, and `c` of type `M`; if `a` is an additive unit (i.e., it has an additive inverse), then the equality `b + a = c + a` is equivalent to `b = c`. This theorem essentially expresses the property of canceling the same additive unit from both sides of an equation in an additive monoid.
More concisely: In an additive monoid, if an element has an additive inverse, then adding it to both sides of an equation equates two elements if and only if they are equal.
|
Units.ext
theorem Units.ext : ∀ {α : Type u} [inst : Monoid α], Function.Injective Units.val
The theorem `Units.ext` states that for all types `α` that have a `Monoid` structure, the function `Units.val` which gets the underlying value in the base `Monoid`, is injective. In other words, if two elements of the type `αˣ` (the units of the monoid `α`) have the same underlying value in the base `Monoid`, then they are the same element.
More concisely: For any type `α` with a `Monoid` structure, the function `Units.val` mapping the units of `α` to their underlying values in the base `Monoid` is an injection.
|
AddUnits.add_left_inj
theorem AddUnits.add_left_inj :
∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α) {b c : α}, b + ↑a = c + ↑a ↔ b = c
This theorem, `AddUnits.add_left_inj`, in Lean 4 is stating that for any type `α` that forms an additive monoid, for any unit `a` of addition, the equality `b + ↑a = c + ↑a` is equivalent to `b = c`. In other words, if adding the same unit to two elements `b` and `c` in the monoid results in the same result, then `b` and `c` must have been the same to begin with. This theorem embodies the concept of left-cancellation in the setting of an additive monoid.
More concisely: For any additive monoid type `α` and unit `a` of addition, `b = c` if and only if `b + a = c + a`.
|
isUnit_of_mul_isUnit_left
theorem isUnit_of_mul_isUnit_left : ∀ {M : Type u_1} [inst : CommMonoid M] {x y : M}, IsUnit (x * y) → IsUnit x := by
sorry
This theorem states that for any type `M` that forms a commutative monoid, if `x` and `y` are elements of `M` and the product `x * y` is a unit (meaning it has a two-sided inverse), then `x` is also a unit. In other words, if `x * y` has a two-sided inverse in the commutative monoid, then `x` must also have a two-sided inverse.
More concisely: If `M` is a commutative monoid and `x` in `M` has a two-sided inverse when multiplied with `y` in `M`, then `x` is a unit in `M`.
|
AddUnits.val_add
theorem AddUnits.val_add : ∀ {α : Type u} [inst : AddMonoid α] (a b : AddUnits α), ↑(a + b) = ↑a + ↑b
This theorem states that for any type `α` that forms an additive monoid, for any two additive units `a` and `b` of type `α`, the additive operation of the underlying units of `a` and `b` (i.e., `↑a + ↑b`) is equal to the underlying unit of the additive operation of `a` and `b` (i.e., `↑(a + b)`). In other words, applying the additive operation before or after lifting to the additive units doesn't change the result. This is a statement about the compatibility of the additive operation with the embedding from `α` to the additive units.
More concisely: For any additive monoid type `α` and additive units `a` and `b` in `α`, `↑(a + b) = ↑a + ↑b`.
|
IsUnit.mul_val_inv
theorem IsUnit.mul_val_inv : ∀ {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a), a * ↑h.unit⁻¹ = 1
The theorem `IsUnit.mul_val_inv` states that for any type `M` that forms a `Monoid`, for any element `a` of `M` that is a unit, the product of `a` and the inverse of the unit corresponding to `a` is the multiplicative identity, 1. In other words, for any unit element `a` in a monoid, `a` times its reciprocal equals 1.
More concisely: For any monoid `M` and unit `a` in `M`, `a` multiplied with the multiplicative inverse of `a` equals the identity element of `M`.
|
divp_assoc'
theorem divp_assoc' : ∀ {α : Type u} [inst : Monoid α] (x y : α) (u : αˣ), x * (y /ₚ u) = x * y /ₚ u
This theorem, `divp_assoc'`, states that for any type `α` which forms a monoid, given any three elements `x`, `y` of `α` and `u` which is a unit in `α` (i.e., it has an inverse), the equation `x * (y /ₚ u) = x * y /ₚ u` holds true. This theorem allows the `field_simp` tactic to move all division by units (`/ₚ`) to the right hand side of the equation. Here, the `/ₚ` operator signifies "division by a unit".
More concisely: For any monoid type `α` with unit `u`, the equation `x * (y / u) = x * y / u` holds for all `x, y` in `α`.
|
AddGroup.isAddUnit
theorem AddGroup.isAddUnit : ∀ {α : Type u} [inst : AddGroup α] (a : α), IsAddUnit a
This theorem states that for any type `α` which forms an additive group (denoted by `AddGroup α`), every element `a` of this type is an `AddUnit`. In mathematical terms, this means that every element of the additive group has a two-sided additive inverse, or simply put, for each element there exists another element such that their sum is the additive identity (typically zero).
More concisely: Every element in an additive group has a two-sided additive inverse.
|
Units.mul_inv_eq_iff_eq_mul
theorem Units.mul_inv_eq_iff_eq_mul : ∀ {α : Type u} [inst : Monoid α] (b : αˣ) {a c : α}, a * ↑b⁻¹ = c ↔ a = c * ↑b
This theorem states that for any monoid `α`, given an element `b` from the group of units of `α`, and any two other elements `a` and `c` of `α`, the statement that `a` times the multiplicative inverse of `b` equals `c` is equivalent to the statement that `a` equals `c` times `b`. Here, `αˣ` represents the group of units in `α`, and `b⁻¹` represents the multiplicative inverse of `b`. The theorem captures a key algebraic manipulation rule related to multiplicative inverses in a monoid.
More concisely: For any monoid `α` and units `b` in `α`, the equation `a * b⁻¹ = c` is equivalent to `a = c * b` in `α`.
|
Units.ext_iff
theorem Units.ext_iff : ∀ {α : Type u} [inst : Monoid α] {a b : αˣ}, a = b ↔ ↑a = ↑b
This theorem, `Units.ext_iff`, states that for any type `α` equipped with a monoid structure, two elements `a` and `b` of the units of `α` (denoted `αˣ`) are equal if and only if their underlying elements in `α` are equal. The units of `α` are elements that have multiplicative inverses, and `↑a` and `↑b` represent the underlying elements of `a` and `b` in `α`, respectively. The theorem shows the equivalence between the equality of the unit elements and the equality of their respective underlying elements.
More concisely: For any type `α` with a monoid structure and equipped with inverses, two units `a` and `b` are equal if and only if their underlying elements in `α` are equal.
|
isAddUnit_of_add_eq_zero
theorem isAddUnit_of_add_eq_zero : ∀ {M : Type u_1} [inst : AddCommMonoid M] (a b : M), a + b = 0 → IsAddUnit a := by
sorry
This theorem states that for any type `M` that is an additive commutative monoid, if the addition of two elements `a` and `b` of `M` equals zero, then `a` is an `AddUnit`. In other words, if the sum of two elements in an additive commutative monoid is zero, then the first element has a two-sided additive inverse, which means it is an additive unit.
More concisely: In an additive commutative monoid `M`, if `a` and `b` are elements with `a + b = 0`, then `a` is an additive unit of `M`.
|
IsUnit.div_mul_left
theorem IsUnit.div_mul_left : ∀ {α : Type u} [inst : DivisionMonoid α] {a b : α}, IsUnit b → b / (a * b) = 1 / a := by
sorry
This theorem, `IsUnit.div_mul_left`, states that for any type `α` that forms a `DivisionMonoid`, and for any elements `a` and `b` of this type `α`, if `b` is a unit (meaning it has a two-sided inverse), then the result of dividing `b` by the product of `a` and `b` is equal to the result of dividing 1 by `a`. In simpler terms, if `b` is invertible, then `b` divided by (`a` times `b`) is the same as 1 divided by `a`.
More concisely: For any type `α` that forms a `DivisionMonoid` and has an element `b` with a two-sided inverse, `(b : α) \* b = 1 -> b \* a =^-1 1`, where `a` is any element of `α`.
|
IsAddUnit.add_neg_cancel
theorem IsAddUnit.add_neg_cancel : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α}, IsAddUnit a → a + -a = 0 := by
sorry
The theorem `IsAddUnit.add_neg_cancel` states that for any type `α` with a `SubtractionMonoid` structure and any element `a` of `α` that is an `AddUnit` (i.e., has a two-sided additive inverse), the sum of `a` and its additive inverse `-a` equals zero. This is essentially the principle that any number plus its negative equals zero, generalised to any additive monoid where certain elements have an additive inverse.
More concisely: For any additive monoid type `α` and AddUnit `a` in `α`, `a + (-a) = 0`.
|
AddUnits.add_neg
theorem AddUnits.add_neg : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α), ↑a + ↑(-a) = 0
This theorem, `AddUnits.add_neg`, states that for any type `α` that has an addition operation defined on it such that it forms an additive monoid, for any additive unit `a` on `α`, the sum of `a` and its negative counterpart `-a` equals to zero. This essentially proves the property of additivity in a monoid where adding an element with its additive inverse results in the neutral element, in this case 0.
More concisely: For any additive monoid type `α` with additive unit `a`, `a + (-a) = 0`.
|
AddUnits.neg_add_cancel_left
theorem AddUnits.neg_add_cancel_left :
∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α) (b : α), ↑(-a) + (↑a + b) = b
This theorem, `AddUnits.neg_add_cancel_left`, states that for any type `α` that is an additive monoid and given any element `a` of `AddUnits α` and `b` of α, adding the additive inverse of `a` (`-a`) to the sum of `a` and `b` will cancel `a`, producing `b` as the result. In mathematical terms, this can be written as `(-a) + (a + b) = b` where `a` is an element of the additive units of α and `b` is an element of α.
More concisely: For any additive monoid type `α` and elements `a` in its additive units and `b` in `α`, `-a + (a + b) = b`.
|
Units.val_pow_eq_pow_val
theorem Units.val_pow_eq_pow_val : ∀ {α : Type u} [inst : Monoid α] (a : αˣ) (n : ℕ), ↑(a ^ n) = ↑a ^ n
This theorem states that for any type `α` that forms a monoid and for any unit `a` of type `α` and a natural number `n`, the value of `a` raised to the power of `n` is equal to the value of `a` raised to the power of `n` in the context of monoids. In other words, the power of a unit in a monoid, when coerced to the underlying type, is the same as the power of the coerced unit in the underlying type.
More concisely: For any monoid `α` with unit `a`, and natural number `n`, the coerced power `(a : α) ^ n` equals the underlying power `(a : type α) ^ n`.
|
IsUnit.unit_of_val_units
theorem IsUnit.unit_of_val_units : ∀ {M : Type u_1} [inst : Monoid M] {a : Mˣ} (h : IsUnit ↑a), h.unit = a
This theorem, `IsUnit.unit_of_val_units`, states that for any type `M` that has a `Monoid` structure and for any element `a` in the group of units `Mˣ` that is also a unit in the `Monoid` `M` (as specified by the predicate `IsUnit`), the unit of `a` in the `Monoid` (as obtained from the function `IsUnit.unit`) is equal to `a` itself. In other words, if `a` is a unit (i.e., it has a two-sided inverse) in the `Monoid` `M`, then the unit of `a` derived from `IsUnit.unit` is just `a`.
More concisely: For any type `M` with a `Monoid` structure and any unit `a` in `Mˣ` that is also a unit in `M`, `IsUnit.unit a = a`.
|
AddUnits.val_neg
theorem AddUnits.val_neg : ∀ {α : Type u} [inst : AddMonoid α] (self : AddUnits α), ↑self + self.neg = 0
This theorem states that for any type `α` which has an `AddMonoid` instance, the negation operation `neg` on any element of the `AddUnits` of `α` is the right additive inverse of the corresponding `val` (value) of the element. In other words, the sum of any element and its negation within this additive monoid is zero.
More concisely: For any type `α` with an `AddMonoid` instance and any additive identity element `zero_add` of `α`, if `a` is an element of the additive submonoid of `α` containing `zero_add` and having additive inverses, then `neg a = -a` is the additive inverse of `a`, i.e., `a + neg a = zero_add`.
|
AddUnits.isAddUnit_addUnits_add
theorem AddUnits.isAddUnit_addUnits_add :
∀ {M : Type u_3} [inst : AddMonoid M] (u : AddUnits M) (a : M), IsAddUnit (↑u + a) ↔ IsAddUnit a
The theorem `AddUnits.isAddUnit_addUnits_add` states that for any type `M` which has an AddMonoid structure, for any element `u` of the additive units `AddUnits M` and any element `a` from `M`, the property of `a` being an additive unit (`IsAddUnit a`) is not affected by the addition of `u` on the left (i.e., `IsAddUnit (↑u + a)` is equivalent to `IsAddUnit a`). In other words, adding an additive unit to a element does not change whether or not that element is an additive unit.
More concisely: For any type `M` with AddMonoid structure and any additive unit `u` in `AddUnits M` and any element `a` in `M`, `IsAddUnit a` is equivalent to `IsAddUnit (u + a)`.
|
Units.mul_inv_cancel_right
theorem Units.mul_inv_cancel_right : ∀ {α : Type u} [inst : Monoid α] (a : α) (b : αˣ), a * ↑b * ↑b⁻¹ = a
This theorem states that for any type `α` that is a monoid, and for any elements `a` of type `α` and `b` of type `αˣ` (which means `b` is a unit or invertible element in the monoid), the product of `a` and `b` followed by multiplication by the inverse of `b` is equal to `a`. In mathematical terms, this theorem is stating the property `a * b * b⁻¹ = a` for monoids.
More concisely: For any monoid `α` and invertible element `b` of `α`, the product of any element `a` in `α` with `b` and the inverse of `b` is equal to `a`. In Lean notation, `(a : α) : a * b * b⁻¹ = a`.
|
Units.inv_mul
theorem Units.inv_mul : ∀ {α : Type u} [inst : Monoid α] (a : αˣ), ↑a⁻¹ * ↑a = 1
This theorem states that for any type `α` that forms a monoid (i.e., it has an associative binary operation and an identity element), the inverse of any unit `a` in `α` when multiplied by `a` gives the identity element. In mathematical terms, it's saying that for all `a` in the group of units of `α`, the product of the inverse of `a` and `a` is equal to 1, where 1 is the identity element of the monoid.
More concisely: For any monoid `α` with identity element `e` and unit `a` having an inverse `a⁻¹`, we have `a⁻¹ * a = e`.
|
AddUnits.eq_iff
theorem AddUnits.eq_iff : ∀ {α : Type u} [inst : AddMonoid α] {a b : AddUnits α}, ↑a = ↑b ↔ a = b
This theorem, `AddUnits.eq_iff`, establishes a condition for equality between two additive units `a` and `b` in the context of an additive monoid `α`. Specifically, it states that the coercion of `a` and `b` to `α` are equal if and only if `a` and `b` themselves are equal. This means that if the underlying elements of `a` and `b` in `α` are equal, then the `AddUnits` `a` and `b` must also be equal, and vice versa.
More concisely: Given an additive monoid `α`, for all additive units `a` and `b` in `α`, `a = b` if and only if `coe a = coe b`.
|
Mathlib.Algebra.Group.Units._auxLemma.26
theorem Mathlib.Algebra.Group.Units._auxLemma.26 :
∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : Subsingleton (AddUnits α)] {a b : α},
(a + b = 0) = (a = 0 ∧ b = 0)
This theorem, `Mathlib.Algebra.Group.Units._auxLemma.26`, states that for any type `α` that is an additive commutative monoid (i.e., it supports addition operation that is both commutative and associative, and it has a zero element that acts as an identity for addition) and where `AddUnits α` is a subsingleton (i.e., it contains at most one element), for any two elements `a` and `b` of `α`, the condition `a + b = 0` is equivalent to both `a = 0` and `b = 0`. In simpler terms, if `a` and `b` sum up to zero, then both `a` and `b` must individually be zero.
More concisely: For any additive commutative monoid `α` with a subsingleton set of additive units, the equality of any two elements `a` and `b` to the additive identity implies both `a` and `b` are the additive identity.
|
mul_eq_one
theorem mul_eq_one :
∀ {α : Type u} [inst : CommMonoid α] [inst_1 : Subsingleton αˣ] {a b : α}, a * b = 1 ↔ a = 1 ∧ b = 1
This theorem, `mul_eq_one`, states that for any type `α` that is a commutative monoid, and where `αˣ` (the units of `α`) is a subsingleton (i.e., has at most one element), if the product of any two elements `a` and `b` of `α` equals one, then it is necessary and sufficient that both `a` and `b` are equal to one.
More concisely: For any commutative monoid `α` with a subsingleton unit set, `α × α` consists only of the pair `(1, 1)` if and only if for all `a, b ∈ α`, `a * b = 1` implies `a = b = 1`.
|