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 finsets
and a functionf
froms
toℕ
, ifd = s.gcd
, then thegcd
of(f i) / d
equals1
.finset.int.gcd_div_eq_one
: given a nonempty finsets
and a functionf
froms
toℤ
, ifd = s.gcd
, then thegcd
of(f i) / d
equals1
.finset.polynomial.gcd_div_eq_one
: given a nonempty finsets
and a functionf
froms
toK[X]
, ifd = s.gcd
, then thegcd
of(f i) / d
equals1
.
TODO #
Add a typeclass to state these results uniformly.
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) :