dvd_mul_left
theorem dvd_mul_left : ∀ {α : Type u_1} [inst : CommSemigroup α] (a b : α), a ∣ b * a
This theorem states that for any type `α` that is a commutative semigroup, given any two elements `a` and `b` from `α`, `a` divides the product of `b` and `a`. It means `a` is a factor of `b * a` in the context of this specific algebraic structure.
More concisely: For any commutative semigroup type `α`, and any of its elements `a` and `b`, `a` divides the product `b * a`.
|
Dvd.dvd.pow
theorem Dvd.dvd.pow : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a ∣ b → ∀ {n : ℕ}, n ≠ 0 → a ∣ b ^ n
This theorem, named `Dvd.dvd.pow`, states that in any monoid, if an element `a` divides another element `b`, then `a` also divides any non-zero power of `b`. More formally, given a type `α` that forms a monoid, and two elements `a` and `b` of that type such that `a` divides `b`, for any natural number `n` that is not zero, `a` divides `b` to the power of `n`.
More concisely: If `a` divides `b` in a monoid, then `a` raises to the power of any natural number `n` also divides `b` raised to the power of `n`.
|
dvd_of_mul_right_dvd
theorem dvd_of_mul_right_dvd : ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, a * b ∣ c → a ∣ c
This theorem states that for any type `α` that forms a semigroup, and for any three elements `a`, `b`, and `c` of this type, if `a` multiplied by `b` divides `c`, then `a` also divides `c`. Here, "divides" is represented by the `∣` symbol: `a ∣ c` means that `c` is an integer multiple of `a`.
More concisely: For any semigroup type `α`, if `a` multiplies `b` and the result divides `c` (`a * b ∣ c`), then `a` divides `c` (`a ∣ c`).
|
mul_dvd_mul
theorem mul_dvd_mul : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * d
This theorem states that for any type `α` that forms a commutative semigroup, given any elements `a`, `b`, `c`, and `d` of `α`, if `a` divides `b` and `c` divides `d`, then the product `a * c` divides the product `b * d`. Here, "divides" is a relation expressing that one element can be multiplied by some other to yield a third.
More concisely: If `α` is a commutative semigroup, then for all `a, b, c, d ∈ α`, if `a` divides `b` and `c` divides `d`, then `a * c` divides `b * d`.
|
dvd_mul_right
theorem dvd_mul_right : ∀ {α : Type u_1} [inst : Semigroup α] (a b : α), a ∣ a * b
This theorem, named `dvd_mul_right`, asserts that for any type `α` that forms a semigroup, any element `a` of this type divides the product of `a` and any other element `b` of the same type. In other words, if we multiply `a` by any other element of the semigroup, that result is a multiple of `a` (or, `a` is a factor of `a*b`). This holds true for all elements `a` and `b` in the semigroup.
More concisely: For any semigroup type `α` and elements `a, b` in `α`, `a` divides the product `a * b`.
|
Dvd.dvd.mul_right
theorem Dvd.dvd.mul_right : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ b * c
This theorem, named `Dvd.dvd.mul_right`, is an alias of `dvd_mul_of_dvd_left`. It states that for any type `α` that forms a semigroup, given elements `a`, `b`, and `c` of that semigroup such that `a` divides `b`, then `a` also divides the product of `b` and `c`. In mathematical terms, for any \(a, b, c \in \alpha\) such that \(a | b\), we have \(a | bc\).
More concisely: If `a` divides `b` in a semigroup `α`, then `a` divides the product `bc` in `α`.
|
dvd_trans
theorem dvd_trans : ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ c
This theorem, `dvd_trans`, states that for any type `α` that is a semigroup, if one element `a` divides another element `b`, and `b` divides a third element `c`, then `a` also divides `c`. This is the principle of transitivity applied to the "divides" relation in a semigroup.
More concisely: If `a` divides `b` and `b` divides `c` in a semigroup, then `a` divides `c`.
|
dvd_refl
theorem dvd_refl : ∀ {α : Type u_1} [inst : Monoid α] (a : α), a ∣ a
This theorem states that for any type `α` that is a monoid, any element `a` of this type divides itself. In mathematical terms, this means that for any element `a` in a monoid `α`, there exists some other element in `α` such that when multiplied by `a`, results in `a` again. This element is obviously the multiplicative identity of the monoid.
More concisely: For any monoid `α` and element `a` in `α`, there exists an identity element `e` in `α` such that `a * e = a` and `e * a = a`.
|
Dvd.intro
theorem Dvd.intro : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ b
This theorem, `Dvd.intro`, states that for any type `α` that forms a semigroup, given elements `a`, `b`, and `c` of type `α`, if the product of `a` and `c` equals `b` then `a` divides `b`. In mathematical terms, if $a \cdot c = b$, then $a$ is a divisor of $b$.
More concisely: If `α` is a semigroup and `a`, `b`, `c` are elements of `α` such that `a * c = b`, then `a` divides `b`.
|
mul_dvd_mul_right
theorem mul_dvd_mul_right : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, a ∣ b → ∀ (c : α), a * c ∣ b * c := by
sorry
This theorem, `mul_dvd_mul_right`, states that for any type `α` which is a commutative monoid, and any elements `a`, `b`, and `c` of type `α`, if `a` divides `b`, then `a` multiplied by `c` divides `b` multiplied by `c`. Here, the concept of "divides" is used in the sense of divisibility in commutative monoid, meaning that there exists some `k` of type `α` such that `b` equals `a` multiplied by `k`.
More concisely: If `a` divides `b` in a commutative monoid `α`, then `a * c` divides `b * c` for all `c` in `α`.
|
pow_dvd_pow
theorem pow_dvd_pow : ∀ {α : Type u_1} [inst : Monoid α] {m n : ℕ} (a : α), m ≤ n → a ^ m ∣ a ^ n
This theorem, `pow_dvd_pow`, states that for any type `α` that is a monoid, for any natural numbers `m` and `n`, and for any element `a` of type `α`, if `m` is less than or equal to `n`, then `a` to the power `m` divides `a` to the power `n`. In other words, in a monoid, the power of an element to a smaller or equal exponent always divides the power of that element to a greater or equal exponent.
More concisely: For all monoids type `α`, natural numbers `m ≤ n`, and elements `a` of `α`, `a^m` divides `a^n`.
|
dvd_pow
theorem dvd_pow : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a ∣ b → ∀ {n : ℕ}, n ≠ 0 → a ∣ b ^ n
This theorem states that for any type `α` that forms a monoid, given two elements `a` and `b` of this type, if `a` divides `b`, then `a` also divides `b` to the power `n` for any natural number `n` that is not zero. The notation `a ∣ b` represents the divisibility relation where `a` divides `b`. A monoid is a set equipped with an associative binary operation and an identity element.
More concisely: For any monoid `α` and elements `a, b` in `α`, if `a` divides `b`, then `a` divides `b` raised to any natural power `n` (`n ≠ 0`).
|
dvd_mul_of_dvd_left
theorem dvd_mul_of_dvd_left : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ b * c
This theorem states that for any type `α` that is a semigroup (a mathematical structure with an associative binary operation), given any elements `a`, `b`, and `c` of `α`, if `a` divides `b` then `a` also divides the product of `b` and `c`. In mathematical terms, if $a|b$, then for any $c$, we have $a|bc$. This is a fundamental property of divisibility in algebra.
More concisely: If `α` is a semigroup and `a` divides `b` in `α`, then `a` divides the product `b * c` in `α`.
|
pow_dvd_pow_of_dvd
theorem pow_dvd_pow_of_dvd : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, a ∣ b → ∀ (n : ℕ), a ^ n ∣ b ^ n := by
sorry
This theorem states that for any commutative monoid `α` and any elements `a` and `b` of this monoid, if `a` divides `b`, then `a` raised to any natural number power `n` also divides `b` raised to the same power `n`. This theorem essentially generalizes the property of divisibility under exponentiation in the context of a commutative monoid.
More concisely: For any commutative monoid `α` and elements `a, b` of `α`, if `a` divides `b`, then `a^n` divides `b^n` for all natural numbers `n`.
|
Dvd.intro_left
theorem Dvd.intro_left : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} (c : α), c * a = b → a ∣ b
This theorem, `Dvd.intro_left`, states that for any Commutative Semigroup `α`, given any three elements `a`, `b`, and `c` of `α`, if `c` multiplied by `a` equals `b` (`c * a = b`), then `a` divides `b` (`a ∣ b`). A Commutative Semigroup is a set equipped with an associative multiplication operation that is commutative. This theorem essentially captures the mathematical property that if one number times another equals a third, then the second number divides the third.
More concisely: In a commutative semigroup, if the product of two elements is equal to a third element, then one element divides the other two.
|
dvd_of_mul_right_eq
theorem dvd_of_mul_right_eq : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ b
This theorem, also known as an alias of `Dvd.intro`, states that for any type `α` that forms a semigroup, given any elements `a`, `b`, and `c` of `α`, if the product of `a` and `c` equals `b`, then `a` divides `b`. In other words, if `a * c = b` for some `c`, then `a` is a divisor of `b`.
More concisely: If `α` is a semigroup and `a`, `b`, `c` are elements of `α` such that `a * c = b`, then `a` is a divisor of `b` (i.e., `a | b`).
|
exists_eq_mul_right_of_dvd
theorem exists_eq_mul_right_of_dvd : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b → ∃ c, b = a * c
This theorem states that for any type `α` that forms a semigroup, given any two elements `a` and `b` of this type, if `a` divides `b` (denoted as `a ∣ b`), then there exists another element `c` such that `b` is equal to the product of `a` and `c` (`b = a * c`). Essentially, it states the property of divisibility in semigroups: if one element divides another, the second can be expressed as the first multiplied by some third element.
More concisely: In a semigroup, if one element divides another, then there exists an element such that the second element is their product.
|
Mathlib.Algebra.Divisibility.Basic._auxLemma.2
theorem Mathlib.Algebra.Divisibility.Basic._auxLemma.2 : ∀ {α : Type u_1} [inst : Monoid α] (a : α), (a ∣ a) = True
This theorem, named `Mathlib.Algebra.Divisibility.Basic._auxLemma.2`, states that for any type `α` that forms a monoid, any element `a` of this type `α` divides itself, which is always true. Here, the term "divides" (`∣`) is used in the algebraic sense, meaning that there exists another element in the monoid such that when it is multiplied by `a`, the result is `a` itself.
More concisely: For any monoid `α`, every element `a` in `α` divides itself. (In other words, for all `a` in `α`, there exists `x` in `α` such that `a * x = a`.)
|
exists_eq_mul_left_of_dvd
theorem exists_eq_mul_left_of_dvd : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∃ c, b = c * a := by
sorry
This theorem states that for any commutative semigroup `α` and any elements `a` and `b` of `α`, if `a` divides `b` then there exists an element `c` in `α` such that `b` can be expressed as the product of `c` and `a`. In other words, if `a` is a divisor of `b` in a commutative semigroup, then `b` is equal to `a` multiplied by some element.
More concisely: In a commutative semigroup, if one element is a divisor of another, then they are related by multiplication with some other element in the semigroup.
|
dvd_of_mul_left_dvd
theorem dvd_of_mul_left_dvd : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b c : α}, a * b ∣ c → b ∣ c
This theorem states that, given a commutative semigroup (which is a type of algebraic structure with an associative, commutative operation) and three elements `a`, `b`, and `c` of that semigroup, if the product of `a` and `b` divides `c` (denoted by `a * b ∣ c`), then `b` also divides `c` (denoted by `b ∣ c`). This holds true for any arbitrary type `α` which has a commutative semigroup structure.
More concisely: If `a`, `b`, and `c` are elements of a commutative semigroup `α`, then `a * b ∣ c` implies `b ∣ c`.
|
Mathlib.Algebra.Divisibility.Basic._auxLemma.3
theorem Mathlib.Algebra.Divisibility.Basic._auxLemma.3 :
∀ {α : Type u_1} [inst : CommSemigroup α] (a b : α), (a ∣ b * a) = True
This theorem, `Mathlib.Algebra.Divisibility.Basic._auxLemma.3`, states that for any type `α` that has the structure of a commutative semigroup, given any two elements `a` and `b` of that type, `a` divides the product of `b` and `a`. In other words, for all `a` and `b` in a commutative semigroup, `a` is a divisor of `b` multiplied by `a`.
More concisely: For any commutative semigroup type `α`, and any of its elements `a` and `b`, `a` is a divisor of the product `b * a`.
|
Dvd.elim
theorem Dvd.elim : ∀ {α : Type u_1} [inst : Semigroup α] {P : Prop} {a b : α}, a ∣ b → (∀ (c : α), b = a * c → P) → P
This theorem, `Dvd.elim`, states that for any type `α` that forms a semigroup, and for any proposition `P`, if a number `a` divides `b`, then for any number `c` such that `b` equals `a` multiplied by `c`, it implies the proposition `P`. Essentially, it allows us to derive a proposition `P` from the fact that `a` divides `b` in the context of a semigroup.
More concisely: If `α` is a semigroup and `a` divides `b` in `α`, then for any `c` such that `b = a * c`, we have `P`.
|
dvd_of_mul_left_eq
theorem dvd_of_mul_left_eq : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} (c : α), c * a = b → a ∣ b
This theorem, `dvd_of_mul_left_eq`, states that for any type `α` that forms a commutative semigroup, and for any elements `a`, `b`, and `c` of type `α`, if `c * a` equals `b`, then `a` divides `b`. In mathematical terms, it means if `b` can be written as the product of `c` and `a`, then `a` is a factor, or divisor, of `b`.
More concisely: If `c * a = b` in a commutative semigroup, then `a` divides `b`.
|
map_dvd
theorem map_dvd :
∀ {M : Type u_2} {N : Type u_3} [inst : Semigroup M] [inst_1 : Semigroup N] {F : Type u_4} [inst_2 : FunLike F M N]
[inst_3 : MulHomClass F M N] (f : F) {a b : M}, a ∣ b → f a ∣ f b
The theorem `map_dvd` is a statement about the behavior of certain function-like objects under divisibility. Specifically, it says that for all types `M` and `N` with a semigroup structure, any instance of `FunLike` from `M` to `N` that also has a multiplication homomorphism structure (`MulHomClass`), and any elements `a` and `b` of `M`, if `a` divides `b` then the image of `a` under the function divides the image of `b` under the same function. This theorem is a property generally expected of homomorphisms in mathematics, and it expresses that homomorphisms, in some sense, preserve the divisibility relationship between elements.
More concisely: If `f` is a homomorphism from a semigroup (M, +) to a semigroup (N, +) and `a` divides `b` in M, then `f(a)` divides `f(b)` in N.
|
Eq.dvd
theorem Eq.dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a = b → a ∣ b
This theorem, `Eq.dvd`, serves as an alias for `dvd_of_eq`. It states that for any type `α` which forms a Monoid, if we have two elements `a` and `b` from this type, and `a` is equal to `b`, then `a` divides `b`. In mathematical terms, if `a = b`, then `a ∣ b`.
More concisely: If `α` is a Monoid type and `a` and `b` are elements of `α` with `a = b`, then `a` divides `b`.
|
Dvd.dvd.mul_left
theorem Dvd.dvd.mul_left : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ c * b
This theorem, `Dvd.dvd.mul_left`, states that for any type `α` that is a commutative semigroup, if an element `a` divides another element `b`, then `a` also divides the product of `b` and any third element `c`. In other words, if `a` is a divisor of `b`, it remains a divisor even after `b` is multiplied by any other element.
More concisely: If `a` divides `b` in a commutative semigroup, then `a` divides the product `b * c` for any `c`.
|
dvd_iff_exists_eq_mul_right
theorem dvd_iff_exists_eq_mul_right : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b ↔ ∃ c, b = a * c := by
sorry
This theorem, named `dvd_iff_exists_eq_mul_right`, establishes an equivalent condition for divisibility in the context of a semigroup. It states that for all types `α` within the semigroup, and for any two elements `a` and `b` in `α`, `a` divides `b` if and only if there exists some element `c` in `α` such that `b` equals `a` multiplied by `c`. The if and only if condition (↔) means that `a` dividing `b` and `b` equalling `a * c` for some `c` are both equivalent statements - each one can be substituted for the other without changing the truth of the statement as a whole.
More concisely: For any semigroup type `α`, and elements `a`, `b` in `α`, `a` divides `b` if and only if there exists some `c` in `α` such that `b = a * c`.
|
one_dvd
theorem one_dvd : ∀ {α : Type u_1} [inst : Monoid α] (a : α), 1 ∣ a
This theorem states that for all types `α` that form a monoid, the multiplicative identity, i.e., 1, divides any element `a` from the set. In simpler terms, in any multiplication system, 1 is a divisor of every element in the system.
More concisely: For all types `α` forming a monoid, the multiplicative identity `1` is a divisor of every element `a` in `α`.
|
exists_dvd_and_dvd_of_dvd_mul
theorem exists_dvd_and_dvd_of_dvd_mul :
∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : DecompositionMonoid α] {b c a : α},
a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
This theorem states that for any type `α` that is a semigroup and a decomposition monoid, and for any elements `a`, `b`, and `c` of this type, if `a` divides the product of `b` and `c`, then there exist elements `a₁` and `a₂` such that `a₁` divides `b`, `a₂` divides `c`, and `a` is the product of `a₁` and `a₂`. In mathematical terms, given a | b * c, there exist a₁ and a₂ such that a₁ | b, a₂ | c, and a = a₁ * a₂. This theorem essentially states a property of divisibility in the context of certain algebraic structures.
More concisely: If `α` is a semigroup and decomposition monoid, then for any `a, b, c` in `α` with `a | b * c`, there exist `a₁, a₂` in `α` such that `a = a₁ * a₂` with `a₁ | b` and `a₂ | c`.
|
dvd_pow_self
theorem dvd_pow_self : ∀ {α : Type u_1} [inst : Monoid α] (a : α) {n : ℕ}, n ≠ 0 → a ∣ a ^ n
This theorem states that for any type `α` which forms a Monoid, and any element `a` of type `α`, `a` divides `a` to the power of `n` for any natural number `n` that is not zero. In mathematical terms, if `a` is an element of a Monoid and `n` is a non-zero natural number, then `a` divides `a^n`.
More concisely: For any monoid `α` and its element `a`, and any non-zero natural number `n`, `a` divides `a^n`.
|
Dvd.dvd.trans
theorem Dvd.dvd.trans : ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ c
This theorem, called `Dvd.dvd.trans`, is essentially an alias for the `dvd_trans` theorem. It states that for any type `α` that forms a semigroup, if `a` divides `b` and `b` divides `c`, then `a` also divides `c`. In mathematical notation, this is: \(a \,|\, b\), \(b \,|\, c\) ⇒ \(a \,|\, c\). This theorem is a fundamental property of divisibility in the realm of abstract algebra.
More concisely: If `a` divides `b` and `b` divides `c`, then `a` divides `c` (transitivity of divisibility).
|
dvd_rfl
theorem dvd_rfl : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, a ∣ a
This theorem, `dvd_rfl`, states that for any type `α` which forms a monoid, any element `a` of this type divides itself. In the language of divisibility in number theory, if `α` is an integer, then for any integer `a`, `a` divides `a`. This is a universal property in the context of monoids.
More concisely: For any monoid type `α`, every element `a` of `α` divides itself.
|
dvd_mul_of_dvd_right
theorem dvd_mul_of_dvd_right : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ c * b := by
sorry
This theorem, `dvd_mul_of_dvd_right`, states that for any commutative semigroup of type α, if a number `a` divides another number `b`, then `a` also divides the product of `b` and any other number `c`. In mathematical terms, if `a ∣ b` then `a ∣ c * b`, for all `c` in the semigroup. The commutative semigroup property ensures that the multiplication operation is both associative and commutative.
More concisely: If `a` divides `b` in a commutative semigroup, then `a` divides the product `b * c` for all `c` in the semigroup.
|
Mathlib.Algebra.Divisibility.Basic._auxLemma.1
theorem Mathlib.Algebra.Divisibility.Basic._auxLemma.1 :
∀ {α : Type u_1} [inst : Semigroup α] (a b : α), (a ∣ a * b) = True
This theorem, titled `Mathlib.Algebra.Divisibility.Basic._auxLemma.1`, states that for any semigroup `α`, and any elements `a` and `b` of this semigroup, `a` always divides the product `a * b`. In the context of semigroups, "divides" means that there is another element in the semigroup such that `a` times this element equals `a * b`. In this case, the theorem is trivially true as the other element can be `b`.
More concisely: In any semigroup, every element divides the product of itself and any other element.
|
mul_dvd_mul_left
theorem mul_dvd_mul_left : ∀ {α : Type u_1} [inst : Monoid α] {b c : α} (a : α), b ∣ c → a * b ∣ a * c
This theorem states that for any type `α` that has a Monoid structure, and for any elements `a`, `b`, and `c` of that type, if `b` divides `c`, then `a * b` divides `a * c`. In mathematical terms, this says that if `b | c`, then `a*b | a*c`, where `|` represents the divisibility relation. This theorem is fundamental in number theory and algebra, stating an important property about multiplication and divisibility.
More concisely: For any type `α` with a Monoid structure and for all elements `a`, `b`, and `c` of `α`, if `b` divides `c`, then `a * b` divides `a * c`. (In other words, `b | c` implies `a * b | a * c` in the divisibility relation.)
|