Multiset.lcm_cons
theorem Multiset.lcm_cons :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α) (s : Multiset α),
(a ::ₘ s).lcm = lcm a s.lcm
The theorem `Multiset.lcm_cons` states that for any type `α` that has a structure of a cancel commutative monoid with zero and a normalized gcd monoid, and given an element `a` of type `α` and a multiset `s` of elements of type `α`, the least common multiple of the multiset obtained by adding `a` to `s` is equal to the least common multiple of `a` and the least common multiple of the multiset `s`. In other words, the least common multiple operation on multisets is compatible with the cons operation.
More concisely: For any cancel commutative monoid with zero and normalized gcd `α`, the least common multiple of an element `a` and a multiset `s` equals the least common multiple of `a` concatenated with multiset `s`.
|
Multiset.gcd_dedup
theorem Multiset.gcd_dedup :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : DecidableEq α]
(s : Multiset α), s.dedup.gcd = s.gcd
This theorem, `Multiset.gcd_dedup`, states that for any type `α` which is a `CancelCommMonoidWithZero` (a commutative monoid with zero where multiplication with a nonzero element is cancellable), a `NormalizedGCDMonoid` (a commutative monoid with a notion of greatest common divisor and a normalization function), and has a decidable equality, the greatest common divisor (gcd) of a multiset `s` of elements of this type doesn't change if the duplicates are removed from `s` (using `Multiset.dedup`). In other words, the gcd of a multiset is equal to the gcd of the same multiset without duplicates.
More concisely: For any commutative monoid with zero, cancellative multiplication, and decidable equality `α`, the greatest common divisor of a multiset in `α` is unchanged when duplicates are removed.
|
Multiset.lcm_dedup
theorem Multiset.lcm_dedup :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : DecidableEq α]
(s : Multiset α), s.dedup.lcm = s.lcm
The `Multiset.lcm_dedup` theorem asserts that for any type `α` that is a cancel commutative monoid with zero, a normalized GCD monoid, and has decidable equality, and for any multiset `s` of the type `α`, the least common multiple (LCM) of the multiset obtained by removing duplicates from `s` is exactly the same as the LCM of `s` itself. In essence, this theorem states that duplicate elements in a multiset do not affect the calculation of the LCM.
More concisely: For any cancel commutative monoid with zero, a normalized GCD monoid, and decidable equality `α`, the LCM of the multiset obtained by removing duplicates from a multiset `s` of type `α` equals the LCM of `s` itself.
|
Multiset.normalize_gcd
theorem Multiset.normalize_gcd :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s : Multiset α),
normalize s.gcd = s.gcd
This theorem states that for any type `α` that forms a `CancelCommMonoidWithZero` and a `NormalizedGCDMonoid`, and for any multiset `s` of this type, the normalization of the greatest common divisor (GCD) of the multiset is equal to the GCD of the multiset itself. In other words, if we take a multiset, compute its GCD, and then normalize this number, we obtain the same result as if we just computed the GCD. This is essentially saying that the GCD of a multiset is already in a normalized form.
More concisely: For any multiset of types `α` that form a `CancelCommMonoidWithZero` and a `NormalizedGCDMonoid`, the normalization of the greatest common divisor of the multiset equals the greatest common divisor itself.
|
Multiset.lcm_singleton
theorem Multiset.lcm_singleton :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {a : α},
{a}.lcm = normalize a
The theorem `Multiset.lcm_singleton` states that for any type `α` that is a cancel commutative monoid with zero and a normalized GCD monoid, and for any element `a` of type `α`, the least common multiple (LCM) of a multiset containing only `a` is equal to the normalized form of `a`. Here, "normalize" means choosing an element of each associate class by multiplying by `normUnit`, and "lcm" represents the concept of least common multiple in the context of multisets.
More concisely: For any cancel commutative monoid with zero and a normalized GCD monoid `α`, the LCM of a multiset containing only `a` is equal to the normalized form of `a`.
|
Multiset.lcm_add
theorem Multiset.lcm_add :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s₁ s₂ : Multiset α),
(s₁ + s₂).lcm = lcm s₁.lcm s₂.lcm
This theorem states that for any two multisets `s₁` and `s₂` of a type `α`, where `α` is a type with a Cancel Commutative Monoid with Zero structure and a Normalized GCD Monoid structure, the least common multiple (LCM) of the multiset resulting from the addition of `s₁` and `s₂` is equal to the least common multiple (LCM) of the LCM of `s₁` and the LCM of `s₂`. In mathematical terms, this theorem asserts the property: `lcm(lcm(s₁), lcm(s₂)) = lcm(s₁ + s₂)`. This is essentially a distributive property of the least common multiple over the addition of multisets.
More concisely: For any two multisets `s₁` and `s₂` of a type `α` with Cancel Commutative Monoid with Zero and Normalized GCD Monoid structures, `lcm(lcm(s₁, s₂), lcm(s₁ + s₂)) = lcm(s₁, s₂)`.
|
Multiset.dvd_gcd
theorem Multiset.dvd_gcd :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Multiset α} {a : α},
a ∣ s.gcd ↔ ∀ b ∈ s, a ∣ b
This theorem states that for any type `α` that is a cancellative commutative monoid with zero and a normalized greatest common divisor (GCD) monoid, a member `a` of this type, and a multiset `s` of elements of this type, `a` divides the GCD of `s` if and only if `a` divides every element `b` in `s`. A cancellative commutative monoid with zero is a mathematical structure where addition and multiplication are defined, multiplication is commutative, there is a zero element, and cancellation law holds for multiplication. A normalized GCD monoid is a monoid where every element has a greatest common divisor and each greatest common divisor can be normalized (its unit factor is removed). This theorem essentially connects the property of one element dividing the GCD of a set to the property of that element dividing each element of the set.
More concisely: For any cancellative commutative monoid with zero and normalized GCD, an element divides the GCD of a set if and only if it divides every element in the set.
|
Multiset.lcm_dvd
theorem Multiset.lcm_dvd :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Multiset α} {a : α},
s.lcm ∣ a ↔ ∀ b ∈ s, b ∣ a
This theorem states that for any type `α` that is a Cancel Commutative Monoid with Zero and a Normalized GCD Monoid, and for any multiset `s` of type `α` and any element `a` of type `α`, the least common multiple (lcm) of the multiset `s` divides `a` if and only if every element `b` in the multiset `s` divides `a`. In brief, the lcm of a multiset is a common multiple that divides another number precisely when every element in the multiset divides that number.
More concisely: For any cancel commutative monoid with zero and normalized GCD `α`, the least common multiple of a multiset `s` in `α` divides every element `a` in `s` if and only if it divides `a`.
|
Multiset.gcd_cons
theorem Multiset.gcd_cons :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α) (s : Multiset α),
(a ::ₘ s).gcd = gcd a s.gcd
The theorem `Multiset.gcd_cons` states that for any type `α` that has the structure of a cancel commutative monoid with zero and also has the structure of a normalized greatest common divisor (GCD) monoid, and for any element `a` of type `α` and any multiset `s` of type `α`, the greatest common divisor of the multiset obtained by adding `a` to `s` is equal to the greatest common divisor of `a` and the greatest common divisor of `s`. This is similar to the property of the GCD operation in number theory context, where the GCD of a number and the GCD of a set of numbers is the same as the GCD of the set obtained by adding the number to the set.
More concisely: Given a cancel commutative monoid with zero and normalized GCD structure, the greatest common divisor of an element and a multiset is equal to the greatest common divisor of the element and the multiset's existing elements.
|