# Documentation

Mathlib.Algebra.GCDMonoid.Div

# 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.

## TODO #

Add a typeclass to state these results uniformly.

theorem Finset.Nat.gcd_div_eq_one {β : Type u_1} {f : β} (s : ) {x : β} (hx : x s) (hfz : f x 0) :
(Finset.gcd s fun b => f b / ) = 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 : } {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 : ) {x : β} (hx : x s) (hfz : f x 0) :
(Finset.gcd s fun b => f b / ) = 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 : } {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} [] {β : Type u_2} {f : β} (s : ) {x : β} (hx : x s) (hfz : f x 0) :
(Finset.gcd s fun b => f b / ) = 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} [] {s : Finset ()} {x : } (hx : x s) (hnz : x 0) :
(Finset.gcd s fun b => b / Finset.gcd s id) = 1