Finset.lcm_dvd_iff
theorem Finset.lcm_dvd_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
{f : β → α} {a : α}, s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a
This theorem states that for any two types `α` and `β`, where `α` is a Cancel Commutative Monoid with zero and a Normalized GCD Monoid, a function `f` from `β` to `α`, a set `s` of type `β`, and an element `a` of type `α`, the least common multiple (lcm) of the set `s` under the function `f` divides `a` if and only if for each element `b` in the set `s`, `f(b)` divides `a`. In simpler terms, this theorem relates the divisibility of a number by the least common multiple of a set to the divisibility of that number by each element of the set.
More concisely: For any Cancel Commutative Monoid with zero and Normalized GCD Monoid `α`, set `s` of elements in a type `β`, function `f` from `β` to `α`, and element `a` of type `α`, `lcm(map f s)` divides `a` if and only if each `b` in `s` has `f(b)` dividing `a`.
|
Finset.dvd_gcd_iff
theorem Finset.dvd_gcd_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
{f : β → α} {a : α}, a ∣ s.gcd f ↔ ∀ b ∈ s, a ∣ f b
The theorem `Finset.dvd_gcd_iff` states that for all sets `s` of type `β` and all functions `f` from `β` to `α`, where `α` is a type with a cancel commutative monoid with zero structure and a normalized gcd monoid structure, a number `a` of type `α` divides the greatest common divisor (gcd) of the set `s` under the function `f` if and only if `a` divides the value of the function `f` for every element `b` in the set `s`.
More concisely: For a set $s$ of type $\beta$, and a function $f$ from $\beta$ to a type $\alpha$ with cancel commutative monoid and normalized gcd monoid structures, $a$ in $\alpha$ divides the greatest common divisor of $f(s)$ if and only if $a$ divides $f(b)$ for all $b$ in $s$.
|
Finset.normalize_gcd
theorem Finset.normalize_gcd :
∀ {α : Type u_2} {β : Type u_3} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
{f : β → α}, normalize (s.gcd f) = s.gcd f
The theorem `Finset.normalize_gcd` asserts that for any finite set `s` of type `β` and any function `f` from `β` to `α`, where `α` is a type equipped with a `CancelCommMonoidWithZero` and a `NormalizedGCDMonoid` structure, the normalized greatest common divisor (`gcd`) of the images of the elements of `s` under `f` is equal to the `gcd` itself. In other words, normalizing the `gcd` does not change its value. This means that the `gcd` is already in its normalized form.
More concisely: For any finite set `s` and function `f` from a type `β` to a type `α` with `CancelCommMonoidWithZero` and `NormalizedGCDMonoid` structures, the normalized greatest common divisor of `f` applied to the elements of `s` equals the ordinary greatest common divisor of these images.
|
Finset.dvd_lcm
theorem Finset.dvd_lcm :
∀ {α : Type u_2} {β : Type u_3} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
{f : β → α} {b : β}, b ∈ s → f b ∣ s.lcm f
The theorem `Finset.dvd_lcm` states that for any types `α` and `β`, given a cancelable commutative monoid with zero for `α` and a normalized GCD monoid for `α`, any finite set `s` of type `β` and a function `f` from `β` to `α`, if an element `b` belongs to the set `s`, then `f(b)` divides the least common multiple (LCM) of the set `s` as mapped by `f`. Essentially, this theorem guarantees that any element's image under `f` is a factor of the LCM of the image of the whole set under `f`.
More concisely: For any cancelable commutative monoid with zero for type `α`, normalized GCD monoid for type `α`, finite set `s` of type `β`, and function `f` from `β` to `α`, if `b ∈ s`, then `f(b)` divides the LCM of the images of `s` under `f`.
|
Finset.extract_gcd
theorem Finset.extract_gcd :
∀ {α : Type u_2} {β : Type u_3} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
(f : β → α), s.Nonempty → ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
The theorem `Finset.extract_gcd` states that for any nonempty finite set `s` of elements of type `β` and a function `f` from `β` to `α`, where `α` is a type with the structure of a cancel commutative monoid with zero and a normalized greatest common divisor (GCD) monoid, there exists a function `g` such that for all elements `b` in `s`, `f(b)` equals the GCD of the set `s` (with respect to the function `f`) times `g(b)`, and the GCD of the set `s` with respect to the function `g` is 1. This theorem essentially says that we can always extract a factor that turns the GCD of the original function to 1, essentially "normalizing" the function `f` by this factor.
More concisely: Given a nonempty finite set `s` of elements from a type `β` and a function `f` from `β` to a cancellative commutative monoid `α` with a normalized greatest common divisor, there exists a function `g` such that for all `b` in `s`, `f(b)` equals the GCD of `s` with respect to `f` times `g(b)`, and the GCD of `s` with respect to `g` is 1.
|
Finset.gcd_insert
theorem Finset.gcd_insert :
∀ {α : Type u_2} {β : Type u_3} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
{f : β → α} [inst_2 : DecidableEq β] {b : β}, (insert b s).gcd f = gcd (f b) (s.gcd f)
The theorem `Finset.gcd_insert` states that for any types `α` and `β`, where `α` is a cancel commutative monoid with zero and a normalized greatest common divisor (GCD) monoid, for any finite set `s` of elements of type `β`, and for any function `f` from `β` to `α`, if we have decidable equality for `β`, then the GCD of the set obtained by inserting an element `b` of type `β` into `s` (under the function `f`) is equal to the GCD of `f(b)` and the GCD of `s` under `f`. This shows how the GCD of a finite set changes when a new element is added to the set.
More concisely: For any cancel commutative monoid with zero and normalized GCD `α`, function `f` from a finite set `s` of type `β` to `α` with decidable equality, and element `b` of type `β`, the GCD of `s ∪ {b}` under `f` equals the GCD of `f(b)` and the GCD of `s` under `f`.
|
Finset.gcd_dvd
theorem Finset.gcd_dvd :
∀ {α : Type u_2} {β : Type u_3} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
{f : β → α} {b : β}, b ∈ s → s.gcd f ∣ f b
The theorem `Finset.gcd_dvd` states that for any types `α` and `β`, given a `CancelCommMonoidWithZero` and a `NormalizedGCDMonoid` instance for `α`, a finite set `s` of type `β`, and a function `f` from `β` to `α`, if `b` is an element of set `s`, then the greatest common divisor of the set `s` (when each element of `s` is mapped to `α` via `f`) divides the function `f` evaluated at `b`. In other words, in mathematical terms, if $b \in s$, then $\gcd_{b' \in s} f(b') | f(b)$.
More concisely: For any `CancelCommMonoidWithZero` and `NormalizedGCDMonoid` types `α`, given a finite set `s` of type `β`, and a function `f` from `β` to `α`, if `b` is an element of set `s`, then the greatest common divisor of the set `{f(x) | x ∈ s}` divides `f(b)`.
|
Finset.lcm_dvd
theorem Finset.lcm_dvd :
∀ {α : Type u_2} {β : Type u_3} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
{f : β → α} {a : α}, (∀ b ∈ s, f b ∣ a) → s.lcm f ∣ a
The theorem `Finset.lcm_dvd` states that for any type `α` that is a cancel commutative monoid with zero and a normalized GCD monoid, and for any finite set `s` of type `β`, if every element `b` in `s`, when mapped to `α` using function `f`, divides `a`, then the least common multiple (lcm) of the set `s` under the function `f` also divides `a`. In mathematical notation, this can be written as: If $f(b) | a$ for all $b \in s$, then $\operatorname{lcm}(s,f) | a$.
More concisely: If `f : α -> α` maps every element `b` in a finite set `s` of type `β` to a factor of `a` in a cancel commutative monoid with zero and normalized GCD monoid, then the least common multiple of `s` under `f` is a factor of `a`.
|
Finset.gcd_congr
theorem Finset.gcd_congr :
∀ {α : Type u_2} {β : Type u_3} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α]
{s₁ s₂ : Finset β} {f g : β → α}, s₁ = s₂ → (∀ a ∈ s₂, f a = g a) → s₁.gcd f = s₂.gcd g
The theorem `Finset.gcd_congr` states that for any two types `α` and `β` where `α` is a `CancelCommMonoidWithZero` and `NormalizedGCDMonoid`, given two finite sets `s₁` and `s₂` of type `β` and two functions `f` and `g` from `β` to `α`, if `s₁` is equal to `s₂` and, for every element `a` in `s₂`, `f(a)` is equal to `g(a)`, then the greatest common divisor of the set `s₁` under function `f` is equal to the greatest common divisor of the set `s₂` under function `g`. In other words, if two finite sets are the same and the functions applied to their elements yield the same results, then the greatest common divisors of the resulting sets are also equal.
More concisely: If two finite sets of elements from a `CancelCommMonoidWithZero` and `NormalizedGCDMonoid` type, and two functions mapping these elements to the type yield equal sets with equal images for each element, then the greatest common divisors of the sets under these functions are equal.
|
Mathlib.Algebra.GCDMonoid.Finset._auxLemma.1
theorem Mathlib.Algebra.GCDMonoid.Finset._auxLemma.1 :
∀ {α : Type u_1} {β : Type v} {f : α → β} {b : β} {s : Multiset α}, (b ∈ Multiset.map f s) = ∃ a ∈ s, f a = b := by
sorry
This theorem states that for any types `α` and `β`, a function `f` from `α` to `β`, a value `b` of type `β`, and a multiset `s` of type `α`, the value `b` is in the multiset obtained by mapping the function `f` over the multiset `s` if and only if there exists a value `a` in the multiset `s` such that `f(a)` equals `b`. This theorem is a characterization of the membership of an element in the multiset obtained by a function mapping.
More concisely: For any functions $f: \alpha \rightarrow \beta$, values $b \in \beta$, and multisets $s$ of type $\alpha$, $b \in \text{image}(f)(s) \iff \exists a \in s. f(a) = b$.
|
Finset.gcd_eq_zero_iff
theorem Finset.gcd_eq_zero_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
{f : β → α}, s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0
This theorem states that for any types `α` and `β`, given an instance of `α` having a cancel commutative monoid with zero and a NormalizedGCDMonoid structure, and a finite set `s` of type `β` and a function `f` from `β` to `α`, the greatest common divisor of the finite set `s` under function `f` (`Finset.gcd s f`) equals zero if and only if for every element `x` in the set `s`, the function `f` applied to `x` equals zero. Essentially, this theorem provides a condition under which the greatest common divisor of a set of numbers, mapped by a given function, is zero.
More concisely: For any cancel commutative monoids with zero `α` and `β`, and a function `f` from `β` to `α`: The greatest common divisor of a finite set `s` in `β`, under `f`, is zero if and only if `f(x)` is zero for all `x` in `s`.
|