Mathlib.Algebra.Ring.Divisibility.Basic._auxLemma.5
theorem Mathlib.Algebra.Ring.Divisibility.Basic._auxLemma.5 :
∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, (a ∣ -b) = (a ∣ b)
This theorem, named `Mathlib.Algebra.Ring.Divisibility.Basic._auxLemma.5`, states that for any type `α` that forms a semigroup and has the property of distributive negation (`HasDistribNeg`), if we have any two elements `a` and `b` of type `α`, then `a` divides negative `b` if and only if `a` divides `b`. In mathematical terms, it asserts that for any given semigroup elements `a` and `b`, $a | -b$ is equivalent to $a | b$.
More concisely: In a semigroup with distributive negation, the relations $a | b$ and $a | -b$ are equivalent for any $a, b$ in the semigroup.
|
dvd_add_left
theorem dvd_add_left : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ c → (a ∣ b + c ↔ a ∣ b)
The theorem `dvd_add_left` states that for any type `α` that forms a non-unital ring, for any elements `a`, `b`, and `c` of `α`, if `a` divides `c`, then `a` divides the sum of `b` and `c` if and only if `a` divides `b`. In other words, in a non-unital ring, if one element is a divisor of a second element, then it also divides the sum of the second element and a third element if and only if it divides the third element.
More concisely: In a non-unital ring, if `a` divides `c`, then `a` divides `b` if and only if `a` divides `b + c`.
|
dvd_sub_right
theorem dvd_sub_right : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ b → (a ∣ b - c ↔ a ∣ c)
This theorem states that for any non-unital ring `α` and any elements `a`, `b`, and `c` in the ring, if `a` divides `b`, then `a` divides the difference of `b` and `c` if and only if `a` divides `c`. In mathematical terms, it is stating that if `a | b` (read as "a divides b"), then `a | (b - c)` if and only if `a | c`. This theorem is a statement about divisibility in a ring, which is a fundamental concept in algebra.
More concisely: For any non-unital ring `α` and elements `a`, `b`, `c` in `α`, if `a` divides `b`, then `a` divides `b - c` if and only if `a` divides `c`.
|
neg_dvd
theorem neg_dvd : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, -a ∣ b ↔ a ∣ b
This theorem states that for any semigroup (a set with an associative binary operation) that additionally supports distributive negation (negation operation that distributes over the semigroup operation), the negation of an element 'a' divides another element 'b' if and only if 'a' itself divides 'b'. In simpler terms, in this type of semigroup, if 'a' is a factor of 'b', then so is '-a' and vice versa.
More concisely: In a semigroup with distributive negation, the negation of an element is a multiplicative inverse if and only if the original element is.
|
Dvd.dvd.sub
theorem Dvd.dvd.sub : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ b → a ∣ c → a ∣ b - c
This theorem, `Dvd.dvd.sub`, states that for any type `α` that forms a non-unital ring (a ring that may not have a multiplicative identity), if a number `a` divides `b` and `a` divides `c`, then `a` also divides the difference `b - c`. In other words, if `a` is a divisor of both `b` and `c`, then it is also a divisor of the result when `c` is subtracted from `b`.
More concisely: If `a` divides both `b` and `c` in a commutative ring without identity, then `a` divides `b - c`.
|
dvd_sub_self_right
theorem dvd_sub_self_right : ∀ {α : Type u_1} [inst : Ring α] {a b : α}, a ∣ b - a ↔ a ∣ b
This theorem states that for any ring `α` and any two elements `a` and `b` from that ring, the element `a` divides the difference `b - a` if and only if `a` divides `b`. In other words, if `a` is a divisor of the difference between `b` and itself, then it's also a divisor of `b`, and vice versa.
More concisely: For any ring `α` and elements `a, b` in `α`, `a` divides `b - a` if and only if `a` divides `b`.
|
Mathlib.Algebra.Ring.Divisibility.Basic._auxLemma.4
theorem Mathlib.Algebra.Ring.Divisibility.Basic._auxLemma.4 :
∀ {G : Type u_3} [inst : InvolutiveNeg G] {a b : G}, (-a = -b) = (a = b)
This theorem, `Mathlib.Algebra.Ring.Divisibility.Basic._auxLemma.4`, states that for any type `G` equipped with an `InvolutiveNeg` operation, and for any elements `a` and `b` of type `G`, the statement "-a equals -b" is equivalent to the statement "a equals b". In mathematical terms, this theorem says that negating both sides of an equation does not change the truth of the equation.
More concisely: For any type `G` with an `InvolutiveNeg` operation, the negation of an element is the additive inverse, hence `-a = -b` if and only if `a = b`.
|
dvd_sub_self_left
theorem dvd_sub_self_left : ∀ {α : Type u_1} [inst : Ring α] {a b : α}, a ∣ a - b ↔ a ∣ b
This theorem states that for any ring `α` and any elements `a` and `b` of type `α`, `a` divides `a - b` if and only if `a` divides `b`. In mathematical terms, for all `a` and `b` in a given ring, if `a` is a divisor of the difference `a - b`, then it also is a divisor of `b`, and vice versa.
More concisely: For all rings `α` and elements `a, b` of type `α`, `a` divides `b` if and only if `a` divides `a - b`.
|
Dvd.dvd.neg_right
theorem Dvd.dvd.neg_right :
∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, a ∣ b → a ∣ -b
This theorem, named `Dvd.dvd.neg_right`, states that for any type `α` that is a semigroup with a distributive negation, if an element `a` divides another element `b`, then `a` also divides the negative of `b`. In mathematical terms, if `a` divides `b` (denoted as `a ∣ b`), then `a` divides `-b`. This is essentially saying that divisibility is preserved under negation in a semigroup with a distributable negation.
More concisely: If `a` divides `b` in a semigroup with distributive negation, then `a` divides the negation of `b`.
|
dvd_sub_left
theorem dvd_sub_left : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ c → (a ∣ b - c ↔ a ∣ b)
This theorem states that for any types `α` (which forms a non-unital ring), and any three elements `a`, `b`, and `c` of that type, if `a` divides `c` then `a` divides the difference of `b` and `c` if and only if `a` divides `b`. In terms of ring theory, if a number `a` is a divisor of another number `c`, then `a` is a divisor of the difference `b - c` if and only if `a` is also a divisor of `b`.
More concisely: If `α` is a ring type and `a`, `b`, `c` are elements of `α` with `a` dividing `c`, then `a` divides `b - c` if and only if `a` divides `b`.
|
Dvd.dvd.neg_left
theorem Dvd.dvd.neg_left : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, a ∣ b → -a ∣ b
This theorem, `Dvd.dvd.neg_left`, states that for any type `α` that is a semigroup with a distributive negation operation, if an element `a` of this type divides another element `b`, then the negation of `a` also divides `b`. In other words, if `a` divides `b`, then so does `-a`.
More concisely: If `a` divides `b` in a semigroup with distributive negation, then `-a` also divides `b`.
|
dvd_add_right
theorem dvd_add_right : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ b → (a ∣ b + c ↔ a ∣ c)
This theorem states that, in any non-unital ring, if a given element 'a' divides another element 'b', then 'a' divides the sum of 'b' and another element 'c' if and only if 'a' divides 'c'. This means that the divisibility of 'a' in the sum 'b + c' solely depends on its divisibility in 'c' when 'a' is already a divisor of 'b'.
More concisely: In a non-unital ring, if 'a' divides 'b', then 'a' divides 'b + c' if and only if 'a' divides 'c'.
|
dvd_add
theorem dvd_add :
∀ {α : Type u_1} [inst : Add α] [inst_1 : Semigroup α] [inst_2 : LeftDistribClass α] {a b c : α},
a ∣ b → a ∣ c → a ∣ b + c
This theorem, `dvd_add`, states that for all types `α` with addition, semigroup, and left distributive properties, if a number `a` divides number `b` and also divides number `c`, then `a` also divides the sum of `b` and `c`. This theorem is a generalized form of the mathematical principle that if a number divides two numbers individually, it also divides their sum.
More concisely: If `a` divides `b` and `c`, then `a` divides `b + c` for types `α` with addition, semigroup, and left distributive properties.
|
Dvd.dvd.add
theorem Dvd.dvd.add :
∀ {α : Type u_1} [inst : Add α] [inst_1 : Semigroup α] [inst_2 : LeftDistribClass α] {a b c : α},
a ∣ b → a ∣ c → a ∣ b + c
This theorem, referred to as an alias of `dvd_add`, states that for any type `α` that supports addition and forms a semigroup and a left distributive class, if a number `a` divides `b` and `a` also divides `c`, then `a` is also a divisor of the sum of `b` and `c`. In mathematical terms, if `a ∣ b` and `a ∣ c`, then `a ∣ (b + c)`.
More concisely: If `a` is a divisor of both `b` and `c`, then `a` is a divisor of their sum `b + c`.
|
dvd_neg
theorem dvd_neg : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, a ∣ -b ↔ a ∣ b
This theorem states that for any element `a` of a semigroup (a group-like structure) that also supports a distributive negation operation, `a` divides the negation of another element `b` if and only if `a` divides `b` itself. In simpler terms, if `a` is a factor of `-b`, then `a` is also a factor of `b`, and vice versa, assuming the operations of the semigroup are compatible with the negation operation.
More concisely: For any element `a` in a semigroup with distributive negation, `a` divides `b` if and only if `a` divides the negation of `b`.
|
Dvd.dvd.of_neg_right
theorem Dvd.dvd.of_neg_right :
∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, a ∣ -b → a ∣ b
This theorem, named `Dvd.dvd.of_neg_right`, states that for any type `α` that is a semigroup and has a distributive negation, an element `a` divides the negation of another element `b` if and only if `a` divides `b`. In simpler terms, if we can evenly divide `a` into `-b`, then we can also evenly divide `a` into `b`. This is part of the algebraic structure theory and is particularly relevant in the study of structures with a negation operation, such as rings and fields.
More concisely: For any semigroup with distributive negation, an element divides the negation of another if and only if it divides that element.
|
Dvd.dvd.of_neg_left
theorem Dvd.dvd.of_neg_left :
∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, -a ∣ b → a ∣ b
This theorem, known as `Dvd.dvd.of_neg_left`, states that for any type `α` that forms a semigroup and has a distributive negation operation, if the negation of an element `a` (denoted as `-a`) divides another element `b` (notated as `-a ∣ b`), then `a` also divides `b` (notated as `a ∣ b`). In other words, this theorem is validating the concept that if the negation of a number is a divisor of another number, then the original number is also a divisor of that other number.
More concisely: If `-a` divides `b` in a semigroup with distributive negation, then `a` divides `b`.
|
dvd_sub
theorem dvd_sub : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ b → a ∣ c → a ∣ b - c
This theorem named `dvd_sub` is a universal statement in the context of a non-unital ring `α`. For any elements `a`, `b`, and `c` in this ring, if `a` divides `b` and `a` divides `c`, then `a` also divides the difference between `b` and `c`. In mathematical terms, it's stating that in a non-unital ring, the divisibility relation is preserved under subtraction.
More concisely: In a non-unital ring, if `a` divides both `b` and `c`, then `a` divides the difference `b - c`.
|
dvd_add_self_left
theorem dvd_add_self_left : ∀ {α : Type u_1} [inst : Ring α] {a b : α}, a ∣ a + b ↔ a ∣ b
This theorem states that for any type `α` that forms a Ring, an element `a` divides the sum of `a` and `b`, if and only if `a` divides `b`. In mathematical terms, it's stating that for any elements `a` and `b` in a ring, $a | (a + b)$ if and only if $a | b$.
More concisely: In a ring, an element `a` divides the sum `a + b` if and only if it divides `b`. Equivalent to: for all rings `R`, all `a, b ∈ R`, `a | (a + b)` if and only if `a | b`.
|
dvd_add_self_right
theorem dvd_add_self_right : ∀ {α : Type u_1} [inst : Ring α] {a b : α}, a ∣ b + a ↔ a ∣ b
This theorem states that for any ring `α` and elements `a` and `b` from `α`, the element `a` divides the sum of `b` and `a` if and only if `a` divides `b`. In mathematical terms, we can say $a$ divides $(b + a)$ if and only if $a$ divides $b$. This theorem basically describes a property of divisibility in the context of ring theory.
More concisely: For any ring element `a` and any other element `b`, `a` divides the sum `b + a` if and only if `a` divides `b`.
|