Mathlib.Algebra.GroupWithZero.Units.Basic._auxLemma.10
theorem Mathlib.Algebra.GroupWithZero.Units.Basic._auxLemma.10 :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, IsUnit a = (a ≠ 0)
This theorem states that for any type `G₀` that is a `GroupWithZero`, an element `a` of `G₀` is a unit (i.e., it has a two-sided inverse) if and only if `a` is not equal to zero. This is expressed in the context of algebraic structures, where a `GroupWithZero` is a group that has an element identified as zero.
More concisely: In the context of groups with zero, an element is a unit if and only if it is not the additive identity.
|
div_eq_one_iff_eq
theorem div_eq_one_iff_eq : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, b ≠ 0 → (a / b = 1 ↔ a = b) := by
sorry
This theorem states that for any type `G₀` that forms a Group with Zero, given any two elements `a` and `b` of `G₀` such that `b` is not equal to zero, the statement "`a` divided by `b` equals 1" is equivalent to the statement "`a` equals `b`". This proposition is foundational in algebra where the rule of division states that any number divided by itself equals 1.
More concisely: For any group with zero `G₀` and non-zero elements `a` and `b` in `G₀`, `a = b` if and only if `a / b = 1`.
|
eq_div_of_mul_eq
theorem eq_div_of_mul_eq : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, c ≠ 0 → a * c = b → a = b / c := by
sorry
This theorem states that for any type `G₀` that has a 'Group with Zero' structure (a multiplication operation that is associative, commutative and has an identity, namely zero), and for any three elements `a`, `b`, and `c` from this type where `c` is not zero, if the multiplication of `a` and `c` equals `b`, then `a` equals `b` divided by `c`. In other words, the theorem is saying that if `a * c = b`, then `a` is equal to `b / c`, provided `c` is not zero.
More concisely: Given a group with zero `G₀` and `a`, `b`, `c` in `G₀` with `c ≠ 0`, if `a * c = b`, then `a = b / c`.
|
IsUnit.ne_zero
theorem IsUnit.ne_zero :
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Nontrivial M₀] {a : M₀}, IsUnit a → a ≠ 0
This theorem states that for any nontrivial monoid with zero (`MonoidWithZero`), which is a monoid that has an additional zero element distinct from the identity, any element `a` of this monoid that is a unit (i.e., has a two-sided inverse), is not equal to zero. In other words, in such a monoid, all unit elements are nonzero.
More concisely: In a `MonoidWithZero`, every unit is non-zero.
|
Ne.isUnit
theorem Ne.isUnit : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → IsUnit a
This theorem, referred to as `Ne.isUnit`, states that for any type `G₀` that is equipped with a `GroupWithZero` structure, if an element `a` of `G₀` is not equal to zero, then `a` is a unit. In terms of algebra, this means that for any element in a group with a distinguished zero element, if the element is not the zero element, then it has a multiplicative inverse, or in other words, it is "invertible" or a "unit".
More concisely: In a group with zero, if an element is non-zero, then it is a unit (has a multiplicative inverse).
|
Ring.inverse_unit
theorem Ring.inverse_unit : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (u : M₀ˣ), Ring.inverse ↑u = ↑u⁻¹
This theorem states that within the context of a monoid with zero `M₀`, for any unit `u` in `M₀` (i.e., any invertible element), the `inverse` function gives the same result as the direct inversion of `u`. In other words, if `x` is an invertible element in `M₀`, then `inverse x` equals to the inverse of `x`, denoted as `x⁻¹`.
More concisely: For any unit `u` in a monoid `M₀` with zero, the function `inverse` and the direct inversion `u⁻¹` are equal: `inverse u = u⁻¹`.
|
IsUnit.mk0
theorem IsUnit.mk0 : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (x : G₀), x ≠ 0 → IsUnit x
The theorem `IsUnit.mk0` states that for any type `G₀` that is an instance of `GroupWithZero`, for any element `x` of `G₀`, if `x` is not equal to zero, then `x` is a unit. In other words, every non-zero element in a group with zero is a unit, i.e., it has a two-sided inverse.
In the context of mathematics, it's essentially stating that in any multiplicative group that includes a zero element (a `GroupWithZero`), every non-zero element is invertible.
More concisely: In a multiplicative group with zero, every non-zero element is a unit and has a two-sided inverse.
|
mul_one_div_cancel
theorem mul_one_div_cancel : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a * (1 / a) = 1
This theorem states that for any type `G₀` that has the structure of a group with zero, for any non-zero element `a` of this group, the product of `a` and the reciprocal of `a` (which is `1 / a`) equals one. In other words, for any non-zero number `a` in such a group, `a` times its reciprocal is always equal to one. This corresponds to the well-known rule in mathematics that a number times its reciprocal equals one.
More concisely: For any group with zero `G₀` and non-zero element `a` in it, `a * (1 / a) = 1`.
|
eq_div_iff
theorem eq_div_iff : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, b ≠ 0 → (c = a / b ↔ c * b = a) := by
sorry
This theorem, `eq_div_iff`, states that for any type `G₀` that is a GroupWithZero (i.e., a mathematical structure with operations of addition and multiplication, a zero element, and an inverse operation for all non-zero elements), given any three elements `a`, `b`, and `c` from `G₀` such that `b` is not zero, `c` is equal to the division of `a` by `b` if and only if the product of `c` and `b` is equal to `a`. This is a generalization of the standard mathematical property $c = \frac{a}{b} \Leftrightarrow cb = a$ for non-zero $b$.
More concisely: For any group with zero `G₀` and non-zero `b` in `G₀`, `c` is the quotient of `a` by `b` if and only if `c` multiplied by `b` equals `a`.
|
div_eq_div_iff
theorem div_eq_div_iff :
∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a b c d : G₀}, b ≠ 0 → d ≠ 0 → (a / b = c / d ↔ a * d = c * b)
This theorem states that for any commutative group with zero (a mathematical structure that has an operation combining elements in a certain way), given non-zero elements `b` and `d`, the equality of the fraction `a / b` and `c / d` is equivalent to the equality of the product `a * d` and `c * b`. In other words, cross multiplying holds in a commutative group with zero.
More concisely: In a commutative group with zero, the equality of `a / b` and `c / d` implies the equality of `a * d` and `b * c`.
|
Units.mk0_val
theorem Units.mk0_val : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (u : G₀ˣ) (h : ↑u ≠ 0), Units.mk0 (↑u) h = u := by
sorry
The theorem `Units.mk0_val` states that for any type `G₀` which is an instance of the `GroupWithZero` class, any non-zero unit `u` in this group, and any proof `h` that the value of `u` is not zero, when we embed `u` into the unit group using the `Units.mk0` function, we get back `u` itself. Basically, this is saying that if we embed a non-zero unit of a group with zero into the unit group, we retrieve the same unit.
More concisely: For any group with zero `G₀` and non-zero unit `u` in `G₀` with proof `h` of non-zero, `Units.mk0 u h` equals `u`.
|
div_div_div_cancel_right
theorem div_div_div_cancel_right :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {b c : G₀} (a : G₀), c ≠ 0 → a / c / (b / c) = a / b
The theorem `div_div_div_cancel_right` is about division in a group with zero. This theorem is applicable for all types `G₀`. It states that for any elements `a`, `b`, and `c` in `G₀`, if `c` is not zero, then the result of dividing `a` by `c` and then dividing this result by the result of `b` divided by `c` is equal to `a` divided by `b`. In simpler terms, it expresses the property that $(a/c)/(b/c) = a/b$, given that $c \neq 0$.
More concisely: If `c` is nonzero in a group `G₀`, then `(a / c) / (b / c) = a / b`.
|
Units.exists_iff_ne_zero
theorem Units.exists_iff_ne_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {x : G₀}, (∃ u, ↑u = x) ↔ x ≠ 0 := by
sorry
This theorem states that for any type `G₀` that forms a `GroupWithZero`, and any element `x` of `G₀`, there exists a unit `u` such that `u` casted to the type `G₀` equals `x` if and only if `x` is not zero. In other words, every non-zero element of a group with zero can be represented as a unit in that group.
More concisely: For any group with zero `G₀` and non-zero element `x` in `G₀`, there exists a unit `u` such that `x = u` in `G₀`.
|
div_eq_div_iff_div_eq_div'
theorem div_eq_div_iff_div_eq_div' :
∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a b c d : G₀}, b ≠ 0 → c ≠ 0 → (a / b = c / d ↔ a / c = b / d)
This theorem, `div_eq_div_iff_div_eq_div'`, asserts that in a `CommGroupWithZero` (a commutative group with an additional distinct zero element), given four elements `a`, `b`, `c`, and `d` where `b` and `c` are not zero, the equality `a / b = c / d` is equivalent to `a / c = b / d`. This means you can interchange the denominators and the equality will still hold, assuming none of the denominators are zero.
More concisely: In a commutative group with additive inverses and a distinct zero element, the quotients `a / b` and `a / c` are equal if and only if `b` and `c` are non-zero and `b = c * d` for some `d`.
|
Units.exists0'
theorem Units.exists0' :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {p : (g : G₀) → g ≠ 0 → Prop},
(∃ g, ∃ (hg : g ≠ 0), p g hg) ↔ ∃ g, p ↑g ⋯
This theorem, `Units.exists0'`, provides an alternative version of `Units.exists0`. It is used in cases where Lean cannot figure out `p` when using `Units.exists0` from right to left. This theorem is for any GroupWithZero `G₀` and any predicate `p` on `G₀` that applies to non-zero elements. It states that there exists a non-zero element `g` of `G₀` for which `p` holds if and only if there exists a unit `g` for which `p` holds when applied to the coerced unit.
More concisely: For any GroupWithZero `G₀` and predicate `p` on non-zero elements, `Units.exists0' G₀ p` is true if and only if there exists a non-zero `g` in `G₀` such that `p g` is true if and only if `p (units g)` is true.
|
isUnit_iff_ne_zero
theorem isUnit_iff_ne_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, IsUnit a ↔ a ≠ 0
This theorem, `isUnit_iff_ne_zero`, states that for any type `G₀` which forms a group with a zero element (captured by the `GroupWithZero G₀` typeclass), and any element `a` of this type, `a` is a unit if and only if `a` is not equal to zero. Here, a unit is defined as an element that has a two-sided inverse.
More concisely: In a group with a zero element, an element is a unit if and only if it is not equal to the zero element.
|
mul_div_mul_right
theorem mul_div_mul_right :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {c : G₀} (a b : G₀), c ≠ 0 → a * c / (b * c) = a / b
This theorem states that for any non-zero element `c` in a group with zero (`G₀`), the equation `a * c / (b * c) = a / b` holds true for any elements `a` and `b` in the group. Essentially, this means that in such a group, the multiplication of `a` and `c` divided by the multiplication of `b` and `c` is equal to the division of `a` by `b`.
More concisely: For any group with zero `G₀` and non-zero element `c`, the quotient of `a * c` by `b * c` equals the quotient of `a` by `b`, for all elements `a` and `b` in `G₀`.
|
Units.ne_zero
theorem Units.ne_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Nontrivial M₀] (u : M₀ˣ), ↑u ≠ 0 := by
sorry
This theorem states that in any nontrivial monoid with zero (a mathematical structure with a binary operation, an identity element, and a distinguished element called zero), any element of the unit group (elements with multiplicative inverses) is not equal to zero. Therefore, if `u` is an element of the unit group in this monoid, it is guaranteed that `u` is not the zero element.
More concisely: In any nontrivial monoid with a zero element, every unit (invertible element) is distinct from zero.
|
div_eq_zero_iff
theorem div_eq_zero_iff : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, a / b = 0 ↔ a = 0 ∨ b = 0
This theorem states that for any type `G₀` equipped with a group with zero structure (denoted `[inst : GroupWithZero G₀]`), and any elements `a` and `b` of this type, the fraction `a / b` is equal to zero if and only if `a` is equal to zero or `b` is equal to zero. In terms of mathematics, it reads: For any elements `a` and `b` in a group with zero, the statement "the division of `a` by `b` is zero" is equivalent to the statement "either `a` is zero or `b` is zero".
More concisely: In a group with zero, the division of two elements is zero if and only if one of them is zero.
|
Mathlib.Algebra.GroupWithZero.Units.Basic._auxLemma.1
theorem Mathlib.Algebra.GroupWithZero.Units.Basic._auxLemma.1 :
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Nontrivial M₀] (u : M₀ˣ), (↑u = 0) = False
This theorem, `Mathlib.Algebra.GroupWithZero.Units.Basic._auxLemma.1`, states that for any nontrivial `MonoidWithZero` (a mathematical structure that is both a monoid and has an element defined as zero), every unit (non-zero element that has a multiplicative inverse) is not equal to zero. In other words, the equality of the unit converted to the monoid type and zero is always false.
More concisely: In any nontrivial MonoidWithZero, a unit is distinct from the zero element.
|
div_mul_div_cancel
theorem div_mul_div_cancel :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {b c : G₀} (a : G₀), c ≠ 0 → a / c * (c / b) = a / b
This theorem states that for any type `G₀` that forms a group with zero, for any non-zero elements `a`, `b`, `c` of `G₀`, the multiplication of `a` divided by `c` and `c` divided by `b` equals `a` divided by `b`. In simpler terms, it describes a property of division and multiplication in the context of a group with zero, where if we divide `a` by `c` and multiply the result by `c` divided by `b`, we'll get the same result as simply dividing `a` by `b`, provided `c` is not zero.
More concisely: In a group with zero, for any non-zero elements `a`, `b`, `c`, `(a / c) * (c / b) = a / b`.
|
div_ne_zero
theorem div_ne_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, a ≠ 0 → b ≠ 0 → a / b ≠ 0
This theorem states that for any type `G₀` which forms a group with a zero element, if we have two elements `a` and `b` from this group, where neither `a` nor `b` are zero, then the division of `a` by `b` (represented as `a / b`) will also be a non-zero element. This is a property of division in groups with a zero element.
More concisely: In a group with a zero element, the quotient of two non-zero elements is a non-zero element.
|
Ring.inverse_mul_cancel
theorem Ring.inverse_mul_cancel :
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x : M₀), IsUnit x → Ring.inverse x * x = 1
The theorem `Ring.inverse_mul_cancel` states that for any type `M₀` which is a `MonoidWithZero`, for every element `x` of `M₀` that is a unit (i.e., it has a two-sided inverse), the product of the `Ring.inverse` of `x` and `x` itself equals `1`. In other words, if `x` in a monoid with zero is invertible, its "inverse" as defined in the `Ring` namespace, when multiplied by `x`, yields the multiplicative identity of the monoid.
More concisely: For any monoid with zero `M₀` and unit `x` in `M₀`, `x * (M₀.inverse x) = 1`.
|
mul_div_mul_left
theorem mul_div_mul_left :
∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {c : G₀} (a b : G₀), c ≠ 0 → c * a / (c * b) = a / b
The theorem `mul_div_mul_left` states that for any type `G₀` that forms a commutative group with zero, and for any non-zero element `c` of `G₀` and any two elements `a` and `b` of `G₀`, the result of multiplying `c` and `a`, then dividing by the product of `c` and `b`, is equal to the result of dividing `a` by `b`. In other words, in a commutative group with zero, `c*a / (c*b) = a / b` for any `a`, `b`, and non-zero `c`.
More concisely: In a commutative group with zero, for all non-zero `c`, `a`, and `b`, `c * a / (c * b) = a / b`.
|
div_mul_cancel_of_imp
theorem div_mul_cancel_of_imp :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, (b = 0 → a = 0) → a / b * b = a
This theorem states that for any type `G₀` that forms a group with zero, and for any elements `a` and `b` of this type, if it is true that `a` equals zero whenever `b` equals zero, then the product of `a` divided by `b` and `b` is always equal to `a`. In mathematical terms, it establishes that if `a = 0` whenever `b = 0`, then `(a / b) * b = a` is always true in the context of a group with zero.
More concisely: If `a = 0` implies `b = 0` in a group with identity `0`, then `(a / b) * b = a`.
|
Ring.mul_inverse_cancel
theorem Ring.mul_inverse_cancel :
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x : M₀), IsUnit x → x * Ring.inverse x = 1
The theorem `Ring.mul_inverse_cancel` states that for any type `M₀` equipped with a structure of monoid with zero, if an element `x : M₀` is a unit (i.e., it has a two-sided inverse), then the product of `x` and its inverse (as defined by `Ring.inverse` function) equals the multiplicative identity of the monoid. In other words, for any invertible element `x`, when you multiply `x` with its inverse, you get back the number one, which is exactly what we expect from the notion of an inverse in a multiplicative monoid.
More concisely: If `x` is an invertible element in a monoid `M₀` with zero, then `x * (Ring.inverse x) = 1`.
|
Ring.inverse_one
theorem Ring.inverse_one : ∀ (M₀ : Type u_2) [inst : MonoidWithZero M₀], Ring.inverse 1 = 1
This theorem states that for any type `M₀` which carries a structure of a monoid with zero, the `Ring.inverse` of the multiplicative identity `1` is `1` itself. This essentially means that `1` is its own multiplicative inverse in any monoid with zero structure.
More concisely: In any monoid with zero, the multiplicative identity has itself as its multiplicative inverse.
|
Mathlib.Algebra.GroupWithZero.Units.Basic._auxLemma.4
theorem Mathlib.Algebra.GroupWithZero.Units.Basic._auxLemma.4 :
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀], IsUnit 0 = (0 = 1)
This theorem states that for any type `M₀` with a structure of `MonoidWithZero` (a monoid that also has a zero element), the zero element of `M₀` is a unit (i.e., has a two-sided inverse) if and only if zero equals one in `M₀`. This is a characterization of units in monoids with zero, in particular, it shows the unusual situation where the zero element could potentially be a unit, which can only occur in a degenerate case where the monoid's unit element is also its zero element.
More concisely: In a monoid with zero, the zero element is its own two-sided inverse if and only if zero equals one.
|
Ring.inverse_eq_inv
theorem Ring.inverse_eq_inv : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a : G₀), Ring.inverse a = a⁻¹
The theorem `Ring.inverse_eq_inv` states that for all elements `a` in a group with zero `G₀`, the `Ring.inverse` of `a` is equal to the inverse of `a`. In other words, in any group with zero, the function `Ring.inverse` acts as the standard group inverse operation for any given element. This is an important property that confirms the consistency of the `Ring.inverse` definition with the standard algebraic concept of an inverse in a group with zero.
More concisely: In a group with zero, the `Ring.inverse` of an element is equal to its group inverse.
|
Ring.inverse_non_unit
theorem Ring.inverse_non_unit : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x : M₀), ¬IsUnit x → Ring.inverse x = 0
This theorem states that for any element `x` in a monoid with zero `M₀`, if `x` is not a unit (i.e., it does not have a two-sided inverse), then the inverse of `x` as defined in the `Ring.inverse` function is zero. This is a direct result of the definition of `Ring.inverse`, which assigns `0` to non-invertible elements of the monoid.
More concisely: If `x` is a non-unit in a monoid `M₀` with zero element, then `Ring.inverse x = 0`.
|
div_eq_iff
theorem div_eq_iff : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, b ≠ 0 → (a / b = c ↔ a = c * b) := by
sorry
This theorem states that for any group with zero of a certain type `G₀`, if `b` is not zero, then `a` divided by `b` equals `c` if and only if `a` equals `c` times `b`. This essentially captures the relationship between division and multiplication in the context of a group with zero.
More concisely: For any group `G` with zero `G₀`, and elements `a`, `b` (with `b ≠ G₀`), `a / b = c` if and only if `a = c * b`.
|
one_div_mul_cancel
theorem one_div_mul_cancel : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → 1 / a * a = 1
This theorem states that for any non-zero element `a` from a type `G₀` that forms a group with zero, the product of `1 / a` and `a` equals 1. In other words, in any mathematical structure that accommodates the concept of a group with zero, such as a field, the reciprocal of `a` times `a` always yields 1 provided that `a` is not zero. This corresponds to the well-known property in field theory that the product of a non-zero number and its reciprocal is always 1.
More concisely: For any non-zero element `a` in a group with identity element `1` (i.e., `G₀` with `0`), `1 / a * a = 1`.
|
div_self
theorem div_self : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a / a = 1
This theorem states that for any non-zero element `a` from a group with zero `G₀`, the division of `a` by itself equals one. This is a common property in mathematics, where any non-zero number divided by itself results in one. The theorem is applicable for any structure that is a Group with zero, meaning it has algebraic operations of addition and multiplication, and contains a zero element.
More concisely: For any group with zero `G₀` and non-zero element `a`, `a * a⁻¹ = 1`. (Here, `a⁻¹` denotes the multiplicative inverse of `a`.)
|
Units.val_mk0
theorem Units.val_mk0 : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (h : a ≠ 0), ↑(Units.mk0 a h) = a := by
sorry
This theorem states that for any given type `G₀` which has the structure of a `GroupWithZero`, and any non-zero element `a` of this group, the value of the unit group element created by the `Units.mk0` function from `a` is equal to `a` itself. In other words, when we embed a non-zero element of a `GroupWithZero` into the unit group using `Units.mk0`, the value of this new unit is just the original element.
More concisely: For any non-zero element `a` in a `GroupWithZero` type `G₀`, the unit group element created by `Units.mk0` from `a` equals `a` itself.
|
not_isUnit_zero
theorem not_isUnit_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Nontrivial M₀], ¬IsUnit 0
This theorem states that for any type `M₀`, if it is equipped with a structure of a `MonoidWithZero` (which is a monoid that has an element called zero that satisfies certain properties) and it is nontrivial (meaning it contains at least two distinct elements), then zero is not a unit in this monoid. In other words, there doesn't exist any element in `M₀` that when multiplied by zero gives the multiplicative identity (which is usually one in the context of monoids).
More concisely: In a nontrivial monoid `M₀` equipped with a `MonoidWithZero` structure, the zero element does not have a multiplicative inverse.
|
mul_div_cancel'
theorem mul_div_cancel' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {b : G₀} (a : G₀), b ≠ 0 → b * (a / b) = a
This theorem, named `mul_div_cancel'`, states that for any type `G₀` that forms a commutative group with zero, for any elements `a` and `b` of that type, if `b` is not equal to zero, then the result of multiplying `b` by the quotient of `a` divided by `b` is equal to `a`. Essentially, this is a formal proof of the well-known mathematical fact that for non-zero `b`, multiplication and division by `b` are inverse operations, or in mathematical symbols, `b * (a / b) = a`.
More concisely: For any commutative group with zero `G₀` and non-zero elements `a` and `b` in `G₀`, `a = b * (a / b)`.
|
Units.exists0
theorem Units.exists0 :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {p : G₀ˣ → Prop},
(∃ g, p g) ↔ ∃ g, ∃ (hg : g ≠ 0), p (Units.mk0 g hg)
This theorem states that for any type `G₀` which has a `GroupWithZero` structure, and any property `p` defined on the group of units in `G₀`, the existence of a unit for which `p` holds is equivalent to the existence of a non-zero element `g` in `G₀` such that `p` holds for the unit constructed using `g` and the proof of `g` not being zero, where the unit is constructed using `Units.mk0` function. In other words, we can rephrase any existence statement about units in `G₀` using the elements of `G₀` and the `Units.mk0` function.
More concisely: For any type `G₀` with a `GroupWithZero` structure and any property `p` on `G₀`'s unit group, the existence of a unit satisfying `p` is equivalent to the existence of a non-zero element `g` in `G₀` such that the unit constructed using `Units.mk0 g` satisfies `p` and `g ≠ 0`.
|
eq_div_iff_mul_eq
theorem eq_div_iff_mul_eq : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, c ≠ 0 → (a = b / c ↔ a * c = b)
This theorem states that for any type `G₀` that has the structure of a group with a distinct zero element (i.e., a "GroupWithZero"), given three elements `a`, `b`, and `c` of this type, with `c` not equal to zero, then `a` is equal to the fraction `b / c` if and only if `a` multiplied by `c` is equal to `b`. This is a standard property of division and multiplication in fields.
More concisely: For any group with zero `G₀` and elements `a`, `b`, and `c` in `G₀` with `c ≠ 0`, `a = b / c` if and only if `a * c = b`.
|