mathlib3documentation

algebra.gcd_monoid.div

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.

TODO #

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 : β } (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 : , b / s.gcd id) = 1