Invertible.congr
theorem Invertible.congr :
∀ {α : Type u} [inst : Monoid α] (a b : α) [inst_1 : Invertible a] [inst_2 : Invertible b], a = b → ⅟a = ⅟b := by
sorry
This theorem states that, given any type `α` that forms a Monoid, if we have two elements `a` and `b` of this type, and both `a` and `b` are invertible, then if `a` equals `b`, the inverse of `a` is equal to the inverse of `b`. In mathematical terms, it asserts that if `a` and `b` are invertible elements of a monoid, and `a = b`, then `⅟a = ⅟b`.
More concisely: If `α` is a monoid type with invertible elements `a` and `b`, then `a = b` implies `⅟a = ⅟b`.
|
invOf_mul_self
theorem invOf_mul_self : ∀ {α : Type u} [inst : Mul α] [inst_1 : One α] (a : α) [inst_2 : Invertible a], ⅟a * a = 1
This theorem states that for any type `α` that has a multiplication operation and a defined element 'one', if we have an element `a` of type `α` which is invertible (has a multiplicative inverse denoted as ⅟a), then the product of ⅟a and `a` is equal to 'one'. This is a formal statement of a fundamental property of multiplicative inverses in the field of mathematics.
More concisely: For any type `α` with multiplication and identity element, if `a` is invertible then `a * ⅟a = one`.
|
invOf_mul_self'
theorem invOf_mul_self' : ∀ {α : Type u} [inst : Mul α] [inst_1 : One α] (a : α) {x : Invertible a}, ⅟a * a = 1 := by
sorry
This theorem states that for any type `α` that supports multiplication and a multiplicative identity (`One`), for any element `a` of such type that is invertible, the product of the inverse of `a` and `a` itself is equal to the multiplicative identity `1`. This is essentially the definition of an inverse element in a multiplicative group, expressed in Lean 4 code.
More concisely: For any type `α` with multiplication and multiplicative identity `One`, and for any invertible element `a` of `α`, `a * a⁻¹ = One`.
|
invOf_mul_self_assoc
theorem invOf_mul_self_assoc : ∀ {α : Type u} [inst : Monoid α] (a b : α) [inst_1 : Invertible a], ⅟a * (a * b) = b
This theorem states that, for any type `α` that forms a monoid (an algebraic structure with a single, associative binary operation and an identity element), given any elements `a` and `b` of this type, where `a` is invertible, multiplying the inverse of `a` (`⅟a`) with the product of `a` and `b` (`a * b`) is equal to `b`. This theorem leverages the property of monoids where each element has an inverse such that the product of an element and its inverse is the identity element. In other words, `⅟a * a = 1` for any invertible `a`.
More concisely: For any monoid `α` with invertible element `a`, `a^-1 * (a * b) = b`.
|
invOf_eq_right_inv
theorem invOf_eq_right_inv : ∀ {α : Type u} [inst : Monoid α] {a b : α} [inst_1 : Invertible a], a * b = 1 → ⅟a = b
This theorem, `invOf_eq_right_inv`, states that for any type `α` that is a monoid, given any elements `a` and `b` of `α`, where `a` is invertible, if the product of `a` and `b` is the identity element of the monoid, then the multiplicative inverse of `a` is `b`. In mathematical notation, this is saying that if `a * b = 1` then `1/a = b` for any invertible element `a` in a monoid.
More concisely: If `a` is an invertible element in a monoid `α` and `a * b = 1`, then `b = 1/a`.
|
mul_invOf_self'
theorem mul_invOf_self' : ∀ {α : Type u} [inst : Mul α] [inst_1 : One α] (a : α) {x : Invertible a}, a * ⅟a = 1 := by
sorry
This theorem, named `mul_invOf_self'`, states that for any type `α` with multiplication and a multiplicative identity (`one`), for any instance `a` of this type that is invertible, the product of `a` and the multiplicative inverse of `a` (`⅟a`) is equal to the multiplicative identity (`1`). In mathematical terms, this can be written as `a * ⅟a = 1`. This is a common property in fields, such as the field of real numbers (`ℝ`).
More concisely: For any type `α` with multiplication and a multiplicative identity `one`, if `a : α` is invertible, then `a * a⁻¹ = one`.
|
Invertible.mul_invOf_self
theorem Invertible.mul_invOf_self :
∀ {α : Type u} [inst : Mul α] [inst_1 : One α] {a : α} [self : Invertible a], a * ⅟a = 1
The theorem `Invertible.mul_invOf_self` states that for any type `α` that supports multiplication and has a multiplicative identity (denoted as `One α`), if a value `a` of type `α` is invertible (meaning there exists an `Invertible a` instance), then the product of `a` and its multiplicative inverse (denoted as `⅟a`) equals the multiplicative identity `1`. In other words, `a` multiplied by its inverse gives `1`. This theorem defines the concept of the "right inverse" in terms of multiplication.
More concisely: For any type `α` with multiplication and multiplicative identity, if `a` is invertible, then `a * ⅟a = One α`.
|
Mathlib.Algebra.Invertible.Defs._auxLemma.2
theorem Mathlib.Algebra.Invertible.Defs._auxLemma.2 :
∀ {G : Type u_1} [inst : Semigroup G] (a b c : G), a * (b * c) = a * b * c
This theorem, from the Mathlib library in Lean 4, states that for any semigroup `G` and any elements `a`, `b`, and `c` of `G`, the operation `a * (b * c)` is equal to `(a * b) * c`. In other words, this theorem asserts the associativity of multiplication in the semigroup: the grouping of factors does not change the result of the multiplication. The semigroup is a set equipped with a binary operation that combines two elements to form a third element in a way that is associative.
More concisely: For any semigroup G and all elements a, b, and c in G, the associativity of multiplication holds: a * (b * c) = (a * b) * c.
|
mul_mul_invOf_self_cancel'
theorem mul_mul_invOf_self_cancel' : ∀ {α : Type u} [inst : Monoid α] (a b : α) {x : Invertible b}, a * b * ⅟b = a := by
sorry
This theorem, `mul_mul_invOf_self_cancel'`, states that for any type `α` that is a monoid (a set with an associative binary operation that has an identity element), and any two elements `a` and `b` of that monoid where `b` is invertible, the product of `a`, `b`, and the inverse of `b` (denoted `⅟b`) is equal to `a`. Essentially, it indicates that multiplying by an element and its inverse cancels out, leaving the other factor unchanged.
More concisely: For all monoids types `α` and invertible elements `a` and `b` in `α`, `a * b * ⅟b = a`.
|
invOf_mul_self_assoc'
theorem invOf_mul_self_assoc' : ∀ {α : Type u} [inst : Monoid α] (a b : α) {x : Invertible a}, ⅟a * (a * b) = b := by
sorry
This theorem states that for any monoid `α`, and any elements `a` and `b` of `α`, if `a` has an inverse, then multiplying the inverse of `a` by the result of `a` and `b` multiplication equals `b`. In terms of mathematical notation, for `a` and `b` in `α` and `a` being invertible, this is saying that ⅟`a` * (`a` * `b`) = `b`.
More concisely: If `a` in monoid `α` has an inverse, then `(a^(-1) * a) * b = b`.
|
mul_invOf_self
theorem mul_invOf_self : ∀ {α : Type u} [inst : Mul α] [inst_1 : One α] (a : α) [inst_2 : Invertible a], a * ⅟a = 1
This theorem, `mul_invOf_self`, states that for any type `α` that supports multiplication and has a multiplicative identity (denoted by `One α`), for any element `a` of this type that is invertible (i.e., has a multiplicative inverse), the result of multiplying `a` by its multiplicative inverse (denoted by `⅟a`) is equal to the multiplicative identity, `1`. This is a formalization of the fundamental property of multiplicative inverses in a multiplicative group.
More concisely: For all types `α` with multiplication and an identity `One α`, and for all invertible elements `a` of `α`, `a * ⅟a = One α`.
|
Invertible.invOf_mul_self
theorem Invertible.invOf_mul_self :
∀ {α : Type u} [inst : Mul α] [inst_1 : One α] {a : α} [self : Invertible a], ⅟a * a = 1
The theorem `Invertible.invOf_mul_self` states that for any type `α` that has a multiplication operation (`Mul α`) and a defined unit (`One α`), for any element `a` of `α` that is invertible (`Invertible a`), the product of the inverse of `a` (`⅟a`) and `a` itself is equal to the identity element (`1`). This is essentially asserting the property that the inverse of a number, when multiplied by the number itself, results in the identity, which is fundamental in the field of mathematics.
More concisely: For any type `α` with multiplication and unit, and for any invertible `a` in `α`, `⅟a * a = 1`.
|