Finset.lcm lemmas

Tags

finset, lcm, prod, coprime

theorem Finset.lcm_dvd_prod {ι : Type u_1} {α : Type u_2} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Finset ι) (f : ι → α) : s.lcm f ∣ s.prod f

theorem Finset.associated_lcm_prod {ι : Type u_1} {α : Type u_2} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset ι} {f : ι → α} (h : (↑s).Pairwise (Function.onFun IsRelPrime f)) : Associated (s.lcm f) (s.prod f)

theorem Finset.lcm_eq_prod {ι : Type u_1} {s : Finset ι} {f : ι → ℕ} (h : (↑s).Pairwise (Function.onFun Nat.Coprime f)) : s.lcm f = s.prod f