Basic results about setwise gcds on normalized gcd monoid with a division. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main results #

finset.nat.gcd_div_eq_one: given a nonempty finset s and a function f from s to ℕ, if d = s.gcd, then the gcd of (f i) / d equals 1.
finset.int.gcd_div_eq_one: given a nonempty finset s and a function f from s to ℤ, if d = s.gcd, then the gcd of (f i) / d equals 1.
finset.polynomial.gcd_div_eq_one: given a nonempty finset s and a function f from s to K[X], if d = s.gcd, then the gcd of (f i) / d equals 1.

Add a typeclass to state these results uniformly.

theorem finset.nat.gcd_div_eq_one {β : Type u_1} {f : β → ℕ} (s : finset β) {x : β} (hx : x ∈ s) (hfz : f x ≠ 0) :

s.gcd (λ (b : β), f b / s.gcd f) = 1

Given a nonempty finset s and a function f from s to ℕ, if d = s.gcd, then the gcd of (f i) / d is equal to 1.

theorem finset.nat.gcd_div_id_eq_one {s : finset ℕ} {x : ℕ} (hx : x ∈ s) (hnz : x ≠ 0) :

s.gcd (λ (b : ℕ), b / s.gcd id) = 1

theorem finset.int.gcd_div_eq_one {β : Type u_1} {f : β → ℤ} (s : finset β) {x : β} (hx : x ∈ s) (hfz : f x ≠ 0) :

s.gcd (λ (b : β), f b / s.gcd f) = 1

Given a nonempty finset s and a function f from s to ℤ, if d = s.gcd, then the gcd of (f i) / d is equal to 1.

theorem finset.int.gcd_div_id_eq_one {s : finset ℤ} {x : ℤ} (hx : x ∈ s) (hnz : x ≠ 0) :

s.gcd (λ (b : ℤ), b / s.gcd id) = 1

theorem finset.polynomial.gcd_div_eq_one {K : Type u_1} [field K] {β : Type u_2} {f : β → polynomial K} (s : finset β) {x : β} (hx : x ∈ s) (hfz : f x ≠ 0) :

s.gcd (λ (b : β), f b / s.gcd f) = 1

Given a nonempty finset s and a function f from s to K[X], if d = s.gcd f, then the gcd of (f i) / d is equal to 1.

theorem finset.polynomial.gcd_div_id_eq_one {K : Type u_1} [field K] {s : finset (polynomial K)} {x : polynomial K} (hx : x ∈ s) (hnz : x ≠ 0) :

s.gcd (λ (b : polynomial K), b / s.gcd id) = 1