Documentation

Mathlib.Algebra.GCDMonoid.Div

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

Main results #

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) :
(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] [DecidableEq 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] [DecidableEq K] {s : Finset (Polynomial K)} {x : Polynomial K} (hx : x s) (hnz : x 0) :
(Finset.gcd s fun (b : Polynomial K) => b / Finset.gcd s id) = 1