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

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) :

(Finset.gcd s fun (b : β) => f b / Finset.gcd s 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) :

(Finset.gcd s fun (b : ℕ) => b / Finset.gcd s id) = 1

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

(Finset.gcd s fun (b : β) => f b / Finset.gcd s 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) :

(Finset.gcd s fun (b : ℤ) => b / Finset.gcd s 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) :

(Finset.gcd s fun (b : β) => f b / Finset.gcd s 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) :