map_invOf
theorem map_invOf :
∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : MulOneClass R] [inst_1 : Monoid S] [inst_2 : FunLike F R S]
[inst_3 : MonoidHomClass F R S] (f : F) (r : R) [inst_4 : Invertible r] [ifr : Invertible (f r)], f ⅟r = ⅟(f r)
The theorem `map_invOf` states that for any types `R`, `S`, and `F`, given that `R` is a `MulOneClass` (a structure with a multiplication and a neutral element for multiplication), `S` is a `Monoid` (a set with an associative binary operation and an identity element), and `F` is a `FunLike` from `R` to `S` (that is, elements of `F` can be viewed as functions from `R` to `S`), and also given that `F` is a monoid homomorphism from `R` to `S` (that is, it preserves the monoid structure), for any element `f` of `F` and any element `r` of `R` that has an inverse element, the inverse of the image of `r` under `f` is equal to the image under `f` of the inverse of `r`. In mathematical notation, this can be expressed as $f(1/r) = 1/(f(r))$. Note that the condition `Invertible (f r)` can be satisfied by using `letI := Invertible.map f r` before applying this lemma.
More concisely: For any `MulOneClass` type `R`, `Monoid` type `S`, and `FunLike` monoid homomorphism `F` from `R` to `S`, if an element `r` in `R` has an inverse, then `F(r)^(-1) = F(r^(-1))`.
|
Ring.inverse_invertible
theorem Ring.inverse_invertible :
∀ {α : Type u} [inst : MonoidWithZero α] (x : α) [inst_1 : Invertible x], Ring.inverse x = ⅟x
This theorem, `Ring.inverse_invertible`, states that for any type `α` that has a structure of a monoid with zero, for any element `x` of `α` that's invertible, the `Ring.inverse` operation applied to `x` yields the multiplicative inverse of `x`, written as `⅟x`. In other words, if we have an invertible element in a monoid with zero, the `Ring.inverse` function acts as the standard inversion operation.
More concisely: For any monoid with zero `α` and invertible element `x` in `α`, `Ring.inverse x = ⅟x`.
|
isUnit_of_invertible
theorem isUnit_of_invertible : ∀ {α : Type u} [inst : Monoid α] (a : α) [inst_1 : Invertible a], IsUnit a
This theorem states that for any type 'α' that forms a 'Monoid', any element 'a' of 'α' that is invertible is a unit. In mathematical terms, if 'α' is a set equipped with an operation that allows it to form a 'Monoid', and if there exists an element 'a' in 'α' such that it has an inverse (i.e., it is invertible), then 'a' is a unit in the 'Monoid'. A unit in this context is an element that has a two-sided inverse.
More concisely: If 'α' is a monoid and 'a' is an invertible element in 'α', then 'a' is a unit in 'α'.
|
IsUnit.nonempty_invertible
theorem IsUnit.nonempty_invertible : ∀ {α : Type u} [inst : Monoid α] {a : α}, IsUnit a → Nonempty (Invertible a) := by
sorry
The theorem `IsUnit.nonempty_invertible` states that for any type `α` which forms a monoid, and for any element `a` of type `α`, if `a` is a unit (meaning it has a two-sided inverse), then there exists an `Invertible` version of `a`. The `Invertible` type in Lean is used to denote invertible elements in a multiplicative monoid or group, thus the theorem essentially asserts the existence of an invertible counterpart for any unit element in a monoid.
More concisely: For any monoid `α` and unit `a` in `α`, there exists an invertible element in `α` that is the multiplicative inverse of `a`.
|
div_self_of_invertible
theorem div_self_of_invertible : ∀ {α : Type u} [inst : GroupWithZero α] (a : α) [inst_1 : Invertible a], a / a = 1
This theorem, `div_self_of_invertible`, states that for all types `α` which are a `GroupWithZero`, if `a` is an element of `α` and `a` is invertible (i.e., it has a multiplicative inverse), then the division of `a` by itself equals 1. In other words, any invertible element in a group with a zero element divided by itself will always give 1.
More concisely: For all types `α` that are a `GroupWithZero` and for all invertible elements `a` in `α`, `a * a^(-1) = 1`.
|
val_unitOfInvertible
theorem val_unitOfInvertible :
∀ {α : Type u} [inst : Monoid α] (a : α) [inst_1 : Invertible a], ↑(unitOfInvertible a) = a
This theorem states that for any given type 'α' that has a Monoid structure, and for any 'a' in that type 'α' which is invertible, the value of the unit created from the invertible 'a' using the 'unitOfInvertible' function is equal to 'a' itself. In simple terms, it means that if an element is invertible in a particular mathematical structure called Monoid, then creating a unit from this invertible element and extracting its value returns the original element.
More concisely: For any invertible element 'a' in a Monoid type 'α', the unit created from 'a' is equal to 'a' itself (unitOfInvertible 'a' = 'a').
|
div_mul_cancel_of_invertible
theorem div_mul_cancel_of_invertible :
∀ {α : Type u} [inst : GroupWithZero α] (a b : α) [inst_1 : Invertible b], a / b * b = a
This theorem states that for any type `α` that is a group with zero, given two elements `a` and `b` of this type, if `b` is invertible (meaning there exists a multiplicative inverse for `b`), then the result of dividing `a` by `b` and then multiplying by `b` is equal to `a`. In mathematical terms, this is equivalent to saying that for any group with zero and any elements `a` and `b` in that group, if `b` has a multiplicative inverse, then `(a / b) * b = a`.
More concisely: If `α` is a group with zero, `a` and `b` are elements of `α` with `b` invertible, then `(a / b) * b = a`.
|
Mathlib.Algebra.Invertible.Basic._auxLemma.2
theorem Mathlib.Algebra.Invertible.Basic._auxLemma.2 :
∀ {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 inversion monoid structure (i.e., an algebraic structure where division and inversion operations are defined), and for any elements `a`, `b`, `c` of `G`, the product of `a` and the result of `b` divided by `c` is equal to the result of `a` multiplied by `b` divided by `c`. In mathematical notation, this is saying that for all `a`, `b`, `c` in `G`, we have `a * (b / c) = a * b / c`.
More concisely: For all `a`, `b`, `c` in a type `G` with division and inversion monoid structure, `a * (b / c) = a * b / c`.
|