Dvd.dvd.antisymm'
theorem Dvd.dvd.antisymm' :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → b = a
This theorem, referred to as an alias of `dvd_antisymm'`, states that for any type `α` that is a Cancel Commutative Monoid with Zero, and has a Subsingleton instance for non-zero elements, if a divides b and b divides a, then b is equal to a. Here, `a` and `b` are elements of type `α`. In mathematical terms, this is equivalent to saying if `a` and `b` are elements of a ring such that `a` is a divisor of `b` and vice versa, then `a` and `b` are the same element.
More concisely: If `α` is a cancel commutative monoid with zero and has a subsingleton instance for non-zero elements, then for all `a` and `b` in `α`, if `a` divides `b` and `b` divides `a`, then `a` equals `b`.
|
ne_zero_of_dvd_ne_zero
theorem ne_zero_of_dvd_ne_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] {p q : α}, q ≠ 0 → p ∣ q → p ≠ 0
This theorem states that for any type `α` which is a 'MonoidWithZero', if we have two elements `p` and `q` of this type such that `q` is not zero and `p` divides `q`, then `p` cannot be zero. In mathematical terms, for all `p` and `q` in a monoid with zero, if `q` is non-zero and `p` is a divisor of `q`, then `p` must also be non-zero.
More concisely: In a monoid with zero, if a non-zero element has a divisor, then that divisor is non-zero.
|
Dvd.dvd.antisymm
theorem Dvd.dvd.antisymm :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → a = b
This theorem, which is an alias of `dvd_antisymm`, states the principle of antisymmetry for the divisibility relation in the context of a cancellation commutative monoid with zero. In particular, for any types `α` that are cancellation commutative monoids with zero and have only one non-zero element (specified by the `Subsingleton αˣ` instance), if `a` divides `b` and `b` divides `a`, then `a` and `b` must be equal. In mathematical terms, if `a` and `b` are elements of such a type `α` and `a | b` and `b | a`, then `a = b`.
More concisely: In a cancellation commutative monoid with zero and only one non-zero element, if `a` divides `b` and `b` divides `a`, then `a` equals `b`.
|
eq_zero_of_zero_dvd
theorem eq_zero_of_zero_dvd : ∀ {α : Type u_1} [inst : SemigroupWithZero α] {a : α}, 0 ∣ a → a = 0
This theorem states that for any type `α` that forms a `SemigroupWithZero` (which is a type of structure that combines the properties of a semigroup and the existence of a "zero" element), if zero divides some element `a` of this type `α`, then `a` must be equal to zero. In mathematical terms, this theorem refers to the property in ring theory that if zero divides any element in a ring, that element must be zero.
More concisely: If `α` is a type with a `SemigroupWithZero` structure, and there exists an element `a` and another element `z` of type `α` such that `a * x = z` for all `x` in `α`, then `a` is equal to the additive identity (zero) of `α`.
|
Mathlib.Algebra.GroupWithZero.Divisibility._auxLemma.2
theorem Mathlib.Algebra.GroupWithZero.Divisibility._auxLemma.2 :
∀ {α : Type u_1} [inst : SemigroupWithZero α] (a : α), (a ∣ 0) = True
This theorem, named `Mathlib.Algebra.GroupWithZero.Divisibility._auxLemma.2` in Lean 4, states that for any type `α` that is a semigroup with zero, any element `a` of that type divides zero. In other words, in the context of algebra where a semigroup with zero is considered, zero can be expressed as the product of any element and some other element in the set. This is a universal property of zero in the context of divisibility within semigroups.
More concisely: In a semigroup with zero, any element divides zero.
|
mul_dvd_mul_iff_right
theorem mul_dvd_mul_iff_right :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] {a b c : α}, c ≠ 0 → (a * c ∣ b * c ↔ a ∣ b)
This theorem states that for any commutative `CancelMonoidWithZero` type `α`, given two elements `a` and `b` of type `α` and a nonzero element `c` of the same type, `a` multiplied by `c` divides `b` multiplied by `c` if and only if `a` divides `b`. Here, `CancelMonoidWithZero` is a type of algebraic structure in which multiplication is commutative, 0 is the multiplicative identity, and multiplication by a nonzero element is cancellative (that is, if `ac = bc` and `c ≠ 0`, then `a = b`).
More concisely: For any commutative `CancelMonoidWithZero` type `α` and nonzero `c` in `α`, `a * c |- b * c` if and only if `a |- b`, where `*` denotes multiplication and `|-` denotes divisibility.
|
dvd_zero
theorem dvd_zero : ∀ {α : Type u_1} [inst : SemigroupWithZero α] (a : α), a ∣ 0
This theorem states that any element `a` of a type `α` that forms a semigroup with zero divides zero. In mathematical terms, for any `a` in a semigroup-with-zero structure `α`, `a` divides `0`. This is a general property in number theory where any number is a divisor of zero.
More concisely: In any semigroup with zero, every non-zero element is a divisor of zero.
|
zero_dvd_iff
theorem zero_dvd_iff : ∀ {α : Type u_1} [inst : SemigroupWithZero α] {a : α}, 0 ∣ a ↔ a = 0
This theorem states that for any given element `a` in a commutative semigroup that includes zero, there exists another element that, when multiplied by zero, results in `a` if and only if `a` itself is equal to zero. This theorem essentially captures the property of zero in multiplication, as any number multiplied by zero gives zero.
More concisely: For any commutative semigroup with zero, an element multiplies to zero if and only if it is equal to zero.
|
mul_dvd_mul_iff_left
theorem mul_dvd_mul_iff_left :
∀ {α : Type u_1} [inst : CancelMonoidWithZero α] {a b c : α}, a ≠ 0 → (a * b ∣ a * c ↔ b ∣ c)
This theorem states that for any given type `α` that forms a `CancelMonoidWithZero`, and for any three elements `a`, `b`, and `c` of this type, where `a` is not zero, the product of `a` and `b` divides the product of `a` and `c` if and only if `b` divides `c`. In mathematical terms, if α is a cancellative monoid with zero and a ≠ 0, then a*b divides a*c exactly when b divides c.
More concisely: For any cancellative monoid with zero `α` and non-zero elements `a, b, c` in `α`, `a*b` divides `a*c` if and only if `b` divides `c`.
|
dvd_antisymm
theorem dvd_antisymm :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → a = b
This theorem, `dvd_antisymm`, states that for any type `α` that is an instance of the `CancelCommMonoidWithZero` class, meaning it behaves like a communicative monoid with a zero element but also has a cancellation property, and is also a `Subsingleton` of unit type `αˣ` (meaning it has at most one term), given any two elements 'a' and 'b' of type `α`, if 'a' divides 'b' and 'b' divides 'a', then 'a' must be equal to 'b'. This theorem embodies a property of divisibility in number systems that support these operations.
More concisely: If `α` is a `CancelCommMonoidWithZero` type and `αˣ` is a subsingleton, then for all `a, b : α`, if `a` divides `b` and `b` divides `a`, then `a = b`.
|
Mathlib.Algebra.GroupWithZero.Divisibility._auxLemma.1
theorem Mathlib.Algebra.GroupWithZero.Divisibility._auxLemma.1 :
∀ {α : Type u_1} [inst : SemigroupWithZero α] {a : α}, (0 ∣ a) = (a = 0)
This theorem, `Mathlib.Algebra.GroupWithZero.Divisibility._auxLemma.1`, states that for any type `α` that is an instance of a `SemigroupWithZero`, and for any element `a` of type `α`, `0` divides `a` if and only if `a` is equal to `0`. In other words, in any zero-containing semigroup, the only element that zero can divide is zero itself. This is a fundamental property of multiplication in mathematical structures with a zero element.
More concisely: In any semigroup with zero, an element is divisible by zero if and only if it is equal to zero.
|