multiplicity.finite_nat_iff
theorem multiplicity.finite_nat_iff : ∀ {a b : ℕ}, multiplicity.Finite a b ↔ a ≠ 1 ∧ 0 < b
The theorem `multiplicity.finite_nat_iff` states that for any two natural numbers `a` and `b`, the multiplicity of `a` in `b` is finite if and only if `a` is not equal to 1 and `b` is greater than 0. Here, the multiplicity of `a` in `b` refers to the highest power of `a` that divides `b`. This theorem connects the finiteness of this multiplicity with the conditions on the numbers themselves, specifically that `a` is not 1 and `b` is positive.
More concisely: The natural number `a` has finite multiplicity in `b` if and only if `a ≠ 1` and `b` is positive.
|
multiplicity.finite_mul
theorem multiplicity.finite_mul :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p a b : α},
Prime p → multiplicity.Finite p a → multiplicity.Finite p b → multiplicity.Finite p (a * b)
This theorem, `multiplicity.finite_mul`, states that for any type `α` that is a cancellative commutative monoid with zero, for any elements `p`, `a`, and `b` of `α`, if `p` is a prime element and the multiplicity of `p` in `a` and `b` is finite, then the multiplicity of `p` in the product `a * b` is also finite. In other words, if a prime number appears a finite number of times as a factor in `a` and `b`, then it also appears a finite number of times in the product of `a` and `b`.
More concisely: If `α` is a cancellative commutative monoid with zero, `p` is a prime element of `α`, and the multiplicities of `p` in `a` and `b` are finite, then the multiplicity of `p` in the product `a * b` is also finite.
|
multiplicity.finite_iff_dom
theorem multiplicity.finite_iff_dom :
∀ {α : Type u_1} [inst : Monoid α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α},
multiplicity.Finite a b ↔ (multiplicity a b).Dom
The theorem `multiplicity.finite_iff_dom` states that for any type `α` which forms a Monoid and has a decidable relation for divisibility, given two elements `a` and `b` of type `α`, the multiplicity of `a` in `b` is finite if and only if the multiplicity of `a` in `b` is defined. In this context, the multiplicity of `a` in `b` being finite means there exists a natural number `n` such that `a` to the power of `n + 1` does not divide `b`, and the multiplicity of `a` in `b` being defined refers to the largest natural number `n` such that `a` to the power `n` divides `b`.
More concisely: For a monoid type `α` with decidable divisibility relation, the multiplicity of `a` in `b` is finite if and only if it is defined, meaning there exists a natural number `n` such that `a^(n + 1)` does not divide `b`, and `a^n` is the largest power of `a` that divides `b`.
|
multiplicity.multiplicity_eq_zero
theorem multiplicity.multiplicity_eq_zero :
∀ {α : Type u_1} [inst : Monoid α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α},
multiplicity a b = 0 ↔ ¬a ∣ b
The theorem named `multiplicity.multiplicity_eq_zero` states that for any type `α` which has a monoid structure and a decidable relation that determines divisibility, given any two elements `a` and `b` of the type `α`, the multiplicity of `a` in `b` is zero if and only if `a` does not divide `b`. In other words, in the context of numbers, the largest natural number `n` such that `a` to the power of `n` divides `b` is zero if and only if `a` is not a factor of `b`.
More concisely: For any type `α` with a monoid structure and a decidable divisibility relation, the multiplicity of `a` in `b` is zero if and only if `a` does not divide `b`.
|
multiplicity.finite_int_iff
theorem multiplicity.finite_int_iff : ∀ {a b : ℤ}, multiplicity.Finite a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0
This theorem states that for any two integers `a` and `b`, the multiplicity of `a` in `b` is finite if and only if the absolute value of `a` is not equal to 1 and `b` is not equal to 0. Here, the multiplicity of `a` in `b` refers to the greatest exponent `n` such that `a` to the power of `n` divides `b`. The absolute value of an integer is its value disregarding its sign.
More concisely: For integers `a` and `b`, the multiplicity of `a` in `b` is finite if and only if `a ≠ 1` and `b ≠ 0`.
|
multiplicity.not_finite_iff_forall
theorem multiplicity.not_finite_iff_forall :
∀ {α : Type u_1} [inst : Monoid α] {a b : α}, ¬multiplicity.Finite a b ↔ ∀ (n : ℕ), a ^ n ∣ b
The theorem `multiplicity.not_finite_iff_forall` states that for any type `α` that forms a Monoid, and for any elements `a` and `b` of that Monoid, the multiplicity of `a` in `b` is not finite if and only if `a` raised to any natural number `n` divides `b`. In other words, the multiplicity of `a` in `b` being infinite means that for every natural number, `a` to the power of that number will be a divisor of `b`.
More concisely: For any Monoid type `α` and elements `a` and `b` of `α`, the multiplicity of `a` in `b` is not finite if and only if `a` raises to every natural number `n` is a divisor of `b`.
|
has_dvd.dvd.multiplicity_pos
theorem has_dvd.dvd.multiplicity_pos :
∀ {α : Type u_1} [inst : Monoid α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α},
a ∣ b → 0 < multiplicity a b
This theorem, named `has_dvd.dvd.multiplicity_pos`, states that for any type `α` that forms a monoid and any two elements `a` and `b` of this type, if `a` divides `b`, then the multiplicity of `a` in `b` is strictly greater than zero. Here, the multiplicity of `a` in `b` is defined as the largest natural number `n` such that `a^n` divides `b` or infinity if such a natural number does not exist. This theorem is essentially a special case or "alias" of the reverse direction of another theorem `multiplicity.dvd_iff_multiplicity_pos`.
More concisely: For any monoid type `α` and elements `a, b` of `α` with `a` dividing `b`, the multiplicity of `a` in `b` is strictly positive.
|
multiplicity.mul
theorem multiplicity.mul :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {p a b : α},
Prime p → multiplicity p (a * b) = multiplicity p a + multiplicity p b
This theorem states that for any type `α` which has a structure of a `CancelCommMonoidWithZero` (a commutative monoid with zero where multiplication has the cancellation property), and a decidable relation which determines if one element divides another, if `p` is a prime element in `α`, then the multiplicity of `p` in the product of `a` and `b` is equal to the sum of the multiplicity of `p` in `a` and the multiplicity of `p` in `b`. In other words, the number of times a prime `p` divides into a product `a * b` is the sum of the number of times `p` divides into `a` and the number of times `p` divides into `b`.
More concisely: For any commutative monoid with zero and cancellation property, and a decidable division relation, if `p` is a prime element, then the multiplicity of `p` in the product of `a` and `b` equals the sum of the multiplicities of `p` in `a` and `b`.
|
multiplicity.unique
theorem multiplicity.unique :
∀ {α : Type u_1} [inst : Monoid α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α} {k : ℕ},
a ^ k ∣ b → ¬a ^ (k + 1) ∣ b → ↑k = multiplicity a b
The theorem `multiplicity.unique` states that for any type `α` that forms a monoid and an operation `∣` which is a decidable relation, if we have elements `a` and `b` of `α` and a natural number `k` such that `a ^ k` divides `b` but `a ^ (k + 1)` does not divide `b`, then `k` equals the multiplicity of `a` in `b`. Here, the multiplicity of `a` in `b` refers to the largest natural number `n` such that `a^n` divides `b`.
More concisely: If `α` is a monoid type with decidable divisibility relation `|`, and `a`, `b` are elements of `α` such that `a^k` divides `b` but `a^(k+1)` does not, then `k` is the multiplicity of `a` in `b`.
|
multiplicity.multiplicity_le_multiplicity_iff
theorem multiplicity.multiplicity_le_multiplicity_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Monoid β] [inst_2 : DecidableRel fun x x_1 => x ∣ x_1]
[inst_3 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α} {c d : β},
multiplicity a b ≤ multiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
The theorem `multiplicity.multiplicity_le_multiplicity_iff` states that for any two types `α` and `β` with `Monoid` structures, and `DecidableRel` relations defined on them as the divisibility relation, given any elements `a` and `b` of type `α`, and `c` and `d` of type `β`, the multiplicity of `a` in `b` is less than or equal to the multiplicity of `c` in `d` if and only if for all natural numbers `n`, if `a` raised to the power `n` divides `b`, then `c` raised to the power `n` divides `d`. Here, the multiplicity of one element in another is defined as the largest natural number `n` such that the first element raised to the power `n` divides the second.
More concisely: The theorem `multiplicity.multiplicity_le_multiplicity_iff` in Lean 4 states that for `Monoid` types `α` and `β` with decidable divisibility relations, the multiplicity of `a` in `b` is less than or equal to the multiplicity of `c` in `d` if and only if for all natural numbers `n`, `a^n` divides `b` implies `c^n` divides `d`.
|
multiplicity.eq_coe_iff
theorem multiplicity.eq_coe_iff :
∀ {α : Type u_1} [inst : Monoid α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α} {n : ℕ},
multiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b
The theorem `multiplicity.eq_coe_iff` states that for a given type `α` forming a monoid, for any two elements `a` and `b` of this type, and a natural number `n`, the multiplicity of `a` in `b` equals `n` if and only if `a` raised to the power of `n` divides `b` and `a` raised to `n + 1` does not divide `b`. In other words, `n` is the largest exponent such that `a^n` divides `b` but `a^(n+1)` does not.
More concisely: For any monoid type `α`, natural number `n`, and elements `a`, `b` of `α`, `a` raised to the power `n` divides `b` and `a` raised to the power `(n+1)` does not divide `b` if and only if the multiplicity of `a` in `b` equals `n`.
|
multiplicity.eq_top_iff_not_finite
theorem multiplicity.eq_top_iff_not_finite :
∀ {α : Type u_1} [inst : Monoid α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α},
multiplicity a b = ⊤ ↔ ¬multiplicity.Finite a b
This theorem, `multiplicity.eq_top_iff_not_finite`, states that for any type `α` which has a monoid structure and a decidable relation for divisibility, given two elements `a` and `b` of `α`, the multiplicity of `a` in `b` is infinity (denoted as `⊤`) if and only if it is not finite. In other terms, for any `a` and `b`, `a` divides `b` infinitely many times if and only if there is no natural number `n` such that `a` to the power of `(n + 1)` does not divide `b`.
More concisely: For any type `α` with a monoid structure and decidable divisibility relation, the multiplicity of `a` in `b` is `⊤` if and only if `a` divides `b` infinitely many times.
|
multiplicity.pow_dvd_of_le_multiplicity
theorem multiplicity.pow_dvd_of_le_multiplicity :
∀ {α : Type u_1} [inst : Monoid α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α} {k : ℕ},
↑k ≤ multiplicity a b → a ^ k ∣ b
The theorem named `multiplicity.pow_dvd_of_le_multiplicity` states that for any type `α` that forms a monoid, and any decidable relation defined by divisibility between two elements of type `α`, along with elements `a` and `b` of this type, and a natural number `k`, if `k` is less than or equal to the multiplicity of `a` in `b`, then `a` to the power of `k` divides `b`.
In mathematical terms, given a monoid with elements `a` and `b`, and a natural number `k`, if `k` is less than or equal to the highest power of `a` that divides `b` (the multiplicity), then `a^k` is a divisor of `b`.
More concisely: If `α` is a monoid with decidable divisibility, `a`, `b` are elements of `α`, and `k` is a natural number less than or equal to the multiplicity of `a` in `b`, then `a^k` divides `b`.
|
multiplicity.pow_dvd_iff_le_multiplicity
theorem multiplicity.pow_dvd_iff_le_multiplicity :
∀ {α : Type u_1} [inst : Monoid α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α} {k : ℕ},
a ^ k ∣ b ↔ ↑k ≤ multiplicity a b
This theorem asserts that for any type `α` equipped with a monoid structure and a decidable relation for divisibility, and for any elements `a` and `b` of type `α` and any natural number `k`, the statement "a raised to the power k divides b" is equivalent to the condition "k is less than or equal to the multiplicity of a in b". Here, the multiplicity of `a` in `b` is the largest natural number `n` such that `a^n` divides `b`. If there is no such `n`, the multiplicity is defined to be infinity.
More concisely: For any monoid `α` with decidable divisibility relation, and for all `a`, `b` in `α` and natural number `k`, `a^k` divides `b` if and only if `k` is less than or equal to the multiplicity of `a` in `b`.
|
multiplicity.is_greatest
theorem multiplicity.is_greatest :
∀ {α : Type u_1} [inst : Monoid α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α} {m : ℕ},
multiplicity a b < ↑m → ¬a ^ m ∣ b
The theorem `multiplicity.is_greatest` states that for any type `α` that has a monoid structure, and any two elements `a` and `b` of that type, along with a natural number `m`, if the multiplicity of `a` in `b` is less than `m`, then `a` raised to the power of `m` does not divide `b`. Here, multiplicity is calculated as the largest natural number `n` such that `a ^ n` divides `b`. This theorem is applicable for any decidable relation for divisibility.
More concisely: For any monoid type `α` and natural numbers `m`, `n`, if the multiplicity of `a` in `b` of type `α` is less than `m`, then `a^m` does not divide `b`.
|
multiplicity.isUnit_right
theorem multiplicity.isUnit_right :
∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α},
¬IsUnit a → IsUnit b → multiplicity a b = 0
The theorem `multiplicity.isUnit_right` states that for any type `α` that has the structure of a commutative monoid and a decidable relation for divisibility, given any two elements `a` and `b` of this type, if `a` is not a unit and `b` is a unit, then the multiplicity of `a` in `b` is zero. Here, a unit is an element that has a two-sided inverse (like 1 in the natural numbers), and the multiplicity of `a` in `b` is the largest natural number `n` such that `a^n` divides `b`. In other words, a non-unit element does not divide a unit element.
More concisely: For any commutative monoid with decidable divisibility relation, a non-unit element does not divide a unit element.
|
multiplicity.exists_eq_pow_mul_and_not_dvd
theorem multiplicity.exists_eq_pow_mul_and_not_dvd :
∀ {α : Type u_1} [inst : Monoid α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α}
(hfin : multiplicity.Finite a b), ∃ c, b = a ^ (multiplicity a b).get hfin * c ∧ ¬a ∣ c
This theorem, named `multiplicity.exists_eq_pow_mul_and_not_dvd`, states that for any type `α` that has a monoid structure and a decidable relation for divisibility, given any two elements `a` and `b` of `α` such that the multiplicity of `a` in `b` is finite (denoted by `multiplicity.Finite a b`), there exists an element `c` of `α` such that `b` equals `a` raised to the power of the multiplicity of `a` in `b` times `c` (expressed as `b = a ^ (multiplicity a b).get hfin * c`), and `a` does not divide `c` (notated as `¬a ∣ c`). In simpler terms, it says that `b` can be expressed as a power of `a` times some `c`, and `a` doesn't divide `c`.
More concisely: For any type `α` with a monoid structure and decidable divisibility relation, given `a` and `b` in `α` such that the multiplicity of `a` in `b` is finite, there exists an element `c` in `α` with `b = a ^ (multiplicity a b) * c` and `a ∣ c ← false`.
|
multiplicity.pow_multiplicity_dvd
theorem multiplicity.pow_multiplicity_dvd :
∀ {α : Type u_1} [inst : Monoid α] [inst_1 : DecidableRel fun x x_1 => x ∣ x_1] {a b : α}
(h : multiplicity.Finite a b), a ^ (multiplicity a b).get h ∣ b
This theorem, `multiplicity.pow_multiplicity_dvd`, asserts that for any type `α` that forms a Monoid, and any two elements `a` and `b` of that type, if `a` has finite multiplicity in `b`, then `b` is divisible by `a` raised to the power of the multiplicity of `a` in `b`. In other words, if `a` appears finitely many times in `b` as a factor, then `b` is divisible by `a` to the power of that count. This theorem is fundamental to understanding the structure of elements in a monoid that can be expressed as products of other elements.
More concisely: For any monoid type `α` and elements `a, b` of `α`, if `a` has finite multiplicity in `b`, then `b` is divisible by `a` raised to that power.
|