Units.coe_dvd
theorem Units.coe_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a : α} {u : αˣ}, ↑u ∣ a
This theorem states that for any given type `α` which forms a Monoid, and any element `a` of this type, as well as any unit `u` of this Monoid, the unit `u` divides the element `a`. In other words, in the context of a Monoid, any element of the Monoid can be expressed as a multiple of any unit of the Monoid.
More concisely: For any Monoid `α` and its unit `u`, every element `a` in `α` can be written as `a = u * b` for some `b` in `α`.
|
IsUnit.dvd
theorem IsUnit.dvd : ∀ {α : Type u_1} [inst : Monoid α] {a u : α}, IsUnit u → u ∣ a
The theorem `IsUnit.dvd` states that, for any type `α` that forms a Monoid, if an element `u` of this Monoid is a unit (i.e., it has a two-sided inverse), then `u` divides any element `a` of the Monoid. Here, "divides" means that there exists some element in the Monoid such that when it is multiplied by `u`, it results in `a`.
More concisely: If `α` is a monoid and `u` is a unit in `α`, then for all `a` in `α`, there exists `x` in `α` such that `u * x = a` and `x * u = a`. (Equivalently, `u` divides `a` and `a` divides `u` in the monoid `α`. )
|
isUnit_of_dvd_one
theorem isUnit_of_dvd_one : ∀ {α : Type u_1} [inst : CommMonoid α] {a : α}, a ∣ 1 → IsUnit a
The theorem `isUnit_of_dvd_one` states that for any commutative monoid `α`, if an element `a` of `α` divides the multiplicative identity (1), then `a` is a unit. Here, a unit is an element that has a two-sided inverse. In other words, if `a` is such that there exists another element in `α` such that their product is 1, then `a` has a two-sided inverse, hence it is a unit.
More concisely: If an element of a commutative monoid has a multiplicative inverse, then it is a unit.
|
IsRelPrime.of_mul_left_right
theorem IsRelPrime.of_mul_left_right :
∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsRelPrime (x * y) z → IsRelPrime y z
The theorem `IsRelPrime.of_mul_left_right` states that for any type `α` that forms a commutative monoid, if `x`, `y`, and `z` are elements of `α`, and `x * y` and `z` are relatively prime (meaning that any common divisor of `x * y` and `z` is a unit), then `y` and `z` are also relatively prime. In other words, if a number `z` is relatively prime to the product of two numbers `x` and `y`, then `z` is also relatively prime to `y`.
More concisely: If `x`, `y`, and `z` are elements of a commutative monoid such that `x * y` and `z` are relatively prime, then `y` and `z` are relatively prime.
|
Units.mul_left_dvd
theorem Units.mul_left_dvd : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α} {u : αˣ}, ↑u * a ∣ b ↔ a ∣ b
In a commutative monoid, given two elements `a` and `b`, and a unit `u`, this theorem states that the product of `u` and `a` (left associate of `a`) divides `b` if and only if `a` divides `b`. This means that the divisibility of `b` by `a` is not affected by multiplying `a` with a unit on the left.
More concisely: In a commutative monoid, the element `u` left-multiplying `a` does not affect the divisibility relationship between `a` and `b`, i.e., `a` divides `b` if and only if `u * a` divides `b`.
|
Mathlib.Algebra.Divisibility.Units._auxLemma.1
theorem Mathlib.Algebra.Divisibility.Units._auxLemma.1 :
∀ {α : Type u_1} [inst : Monoid α] {a u : α}, IsUnit u → (u ∣ a) = True
This theorem states that for any type `α` that forms a Monoid, and for any elements `a` and `u` of `α`, if `u` is a unit (meaning it has a two-sided inverse in the Monoid), then `u` divides `a`. Here, the divisibility relation `u ∣ a` is always true if `u` is a unit element, regardless of what `a` is.
More concisely: For any monoid `α` and unit `u` in `α`, `u` divides every element `a` in `α`.
|
Units.dvd_mul_left
theorem Units.dvd_mul_left : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α} {u : αˣ}, a ∣ ↑u * b ↔ a ∣ b
This theorem states that in a commutative monoid (a set equipped with an associative and commutative binary operation that has an identity element), an element `a` divides another element `b` if and only if `a` divides all left associates of `b`. Here, a left associate of `b` is a unit `u` times `b`, where a unit is an element that has a multiplicative inverse. The theorem is applicable for any types `α` for which the `CommMonoid` instance is available.
More concisely: In a commutative monoid, an element `a` divides `b` if and only if it divides all left associates of `b`.
|
IsRelPrime.mul_left
theorem IsRelPrime.mul_left :
∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α} [inst_1 : DecompositionMonoid α],
IsRelPrime x z → IsRelPrime y z → IsRelPrime (x * y) z
The theorem `IsRelPrime.mul_left` states that for any commutative monoid `α` that also has a decomposition monoid structure, and for any elements `x`, `y`, and `z` of `α`, if `x` and `z` are relatively prime and `y` and `z` are relatively prime, then the product of `x` and `y` is also relatively prime to `z`. In mathematical terms, if $\gcd(x, z) = 1$ and $\gcd(y, z) = 1$, then $\gcd(xy, z) = 1$. Here, 'relatively prime' means that the greatest common divisor is a unit (in integers, it's 1).
More concisely: If `α` is a commutative monoid with a decomposition monoid structure, and `x`, `y`, and `z` are elements of `α` such that `x` is relatively prime to `z` and `y` is relatively prime to `z`, then `x * y` is relatively prime to `z`. (Here, "relatively prime" means that the greatest common divisor of `x` and `z`, as well as `y` and `z`, is a unit.)
|
Units.mul_right_dvd
theorem Units.mul_right_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {u : αˣ}, a * ↑u ∣ b ↔ a ∣ b
This theorem states that in a monoid, an element `a` divides another element `b` if and only if all associates of `a` also divide `b`. Here, an associate of `a` is any element that can be obtained by multiplying `a` by a unit `u` (where units are elements with multiplicative inverses). This theorem is applicable to any type `α` that forms a monoid, a structure with an associative binary operation and an identity element.
More concisely: In a monoid, an element `a` divides `b` if and only if all units multiplied with `a` also divide `b`.
|
Units.dvd_mul_right
theorem Units.dvd_mul_right : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {u : αˣ}, a ∣ b * ↑u ↔ a ∣ b
This theorem states that in a monoid (a kind of algebraic structure), an element 'a' divides another element 'b' if and only if 'a' divides all associates of 'b'. Here, 'a' and 'b' are elements of some type 'α', and 'u' is an invertible element (or unit) of 'α'. The symbol '∣' means 'divides'. That is, 'a' divides 'b' if there is some element 'c' such that 'b' equals 'a' times 'c'. The term 'associates of b' refers to all elements that can be obtained by multiplying 'b' by an invertible element.
More concisely: In a monoid, an element 'a' divides another element 'b' if and only if 'a' divides all associates of 'b' (multiplied by some invertible element 'u').
|
IsUnit.dvd_mul_left
theorem IsUnit.dvd_mul_left : ∀ {α : Type u_1} [inst : CommMonoid α] {a b u : α}, IsUnit u → (a ∣ u * b ↔ a ∣ b) := by
sorry
This theorem states that in a commutative monoid, an element `a` divides another element `b` if and only if `a` divides all left associates of `b`. Here, `α` represents the type of the elements of the monoid, and `a`, `b`, and `u` are elements of this type. `u` is specified to be a unit, which means that it has a two-sided inverse. The symbol `∣` indicates the 'divides' relation. The theorem thus characterizes the 'divides' relation in terms of the unit element and the multiplication operation of the monoid.
More concisely: In a commutative monoid with unit `u`, an element `a` divides `b` if and only if it divides all left associates of `b`, i.e., `a ∣ b` if and only if `a ∣ uⁱ * b` for all natural numbers `n`.
|
IsRelPrime.of_mul_left_left
theorem IsRelPrime.of_mul_left_left :
∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsRelPrime (x * y) z → IsRelPrime x z
The theorem `IsRelPrime.of_mul_left_left` states that for any commutative monoid `α`, and any elements `x`, `y`, and `z` of `α`, if `x*y` and `z` are relatively prime (i.e., their only common divisor is a unit), then `x` and `z` are also relatively prime. Simply put, it tells us that if the product of two elements is relatively prime to another element, then each of those two elements is also relatively prime to that other element.
More concisely: If `x`, `y`, and `z` are elements of a commutative monoid such that `x` and `y`, as well as `y` and `z`, are relatively prime, then `x` and `z` are also relatively prime.
|
isUnit_iff_dvd_one
theorem isUnit_iff_dvd_one : ∀ {α : Type u_1} [inst : CommMonoid α] {x : α}, IsUnit x ↔ x ∣ 1
The theorem `isUnit_iff_dvd_one` states that for any commutative monoid `α` and any element `x` of `α`, `x` is a unit if and only if `x` divides `1`. In the context of the monoid, being a unit means that `x` has a two-sided inverse. The phrase "divides `1`" is a way of expressing that there is some element in the monoid such that when it's multiplied by `x`, the result is `1`. So, in simpler terms, an element is a unit, i.e., it has a two-sided inverse, if and only if it can multiply with some element to give `1`.
More concisely: An element `x` of a commutative monoid is a unit if and only if there exists an element `y` such that `x * y = y * x = 1`.
|
isUnit_of_dvd_unit
theorem isUnit_of_dvd_unit : ∀ {α : Type u_1} [inst : CommMonoid α] {x y : α}, x ∣ y → IsUnit y → IsUnit x
The theorem `isUnit_of_dvd_unit` states that for any type `α` which forms a commutative monoid, given two elements `x` and `y` of `α`, if `x` divides `y` and `y` is a unit (meaning, `y` has a multiplicative inverse), then `x` is also a unit. In other words, if an element divides a unit in a commutative monoid, then that element must also be a unit.
More concisely: If `x` divides `y` and `y` is a unit in a commutative monoid, then `x` is a unit.
|
IsRelPrime.symm
theorem IsRelPrime.symm : ∀ {α : Type u_1} [inst : CommMonoid α] {x y : α}, IsRelPrime x y → IsRelPrime y x
The theorem `IsRelPrime.symm` states that for all types `α` that are instances of the `CommMonoid` class, and for all elements `x` and `y` of `α`, the property of being relatively prime is symmetric. This means that if `x` and `y` are relatively prime (i.e., every common divisor of `x` and `y` is a unit), then `y` and `x` are also relatively prime.
More concisely: If `x` and `y` are relatively prime elements of a commutative monoid `α`, then `y` and `x` are also relatively prime.
|
IsUnit.mul_right_dvd
theorem IsUnit.mul_right_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b u : α}, IsUnit u → (a * u ∣ b ↔ a ∣ b) := by
sorry
This theorem states that in a monoid, given elements `a`, `b`, and `u`, where `u` is a unit (meaning that it has a two-sided inverse), the product of `a` and `u` divides `b` if and only if `a` divides `b`. In other words, when a monoid element `a` is multiplied by any unit `u`, its divisibility property with respect to another element `b` remains unchanged.
More concisely: In a monoid with unit `u`, `a` divides `b` if and only if `a * u` divides `b`.
|
IsUnit.mul_left_dvd
theorem IsUnit.mul_left_dvd : ∀ {α : Type u_1} [inst : CommMonoid α] {a b u : α}, IsUnit u → (u * a ∣ b ↔ a ∣ b) := by
sorry
This theorem states that in a commutative monoid, given three elements `a`, `b`, and `u`, if `u` is a unit (meaning that it has a two-sided inverse), then `u` times `a` divides `b` if and only if `a` divides `b`. In other words, multiplying a unit `u` to `a` doesn't change its divisibility property with respect to `b`.
More concisely: In a commutative monoid, if a unit `u` exists such that `a` divides `b`, then `u * a` divides `b` if and only if `a` divides `b`.
|
isRelPrime_mul_unit_left_left
theorem isRelPrime_mul_unit_left_left :
∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsUnit x → (IsRelPrime (x * y) z ↔ IsRelPrime y z)
This theorem states that for any commutative monoid `α`, and for any elements `x`, `y`, and `z` in `α`, if `x` is a unit (that is, it has a two-sided inverse), then `y` and `z` are relatively prime if and only if the product of `x` and `y` and `z` are relatively prime. In other words, multiplying a factor of `y` by a unit does not change the relative primality of `y` and `z`.
In mathematical terms, we say that for any elements `x`, `y`, and `z` of a commutative monoid, if `x` is a unit, then `y` and `z` are relatively prime if and only if `xy` and `z` are relatively prime. Here, two elements are called relatively prime if their greatest common divisor is a unit.
More concisely: If `x` is a unit in a commutative monoid `α`, then `y` and `z` are relatively prime if and only if `xy` and `z` are relatively prime.
|
isRelPrime_comm
theorem isRelPrime_comm : ∀ {α : Type u_1} [inst : CommMonoid α] {x y : α}, IsRelPrime x y ↔ IsRelPrime y x
The theorem `isRelPrime_comm` states that for any commutative monoid `α` and any elements `x` and `y` in `α`, `x` and `y` being relatively prime is equivalent to `y` and `x` being relatively prime. In other words, the property of being relatively prime is symmetric. Here, two elements `x` and `y` are defined to be relatively prime if every common divisor of `x` and `y` is a unit (i.e., has a multiplicative inverse).
More concisely: For any commutative monoid with units, x and y being relatively prime is equivalent to y and x being relatively prime.
|