Finset.lcm lemmas

Tags

finset, lcm, prod, coprime, Rat.den

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

theorem Finset.associated_lcm_prod {ι : Type u_1} {α : Type u_2} [CommMonoidWithZero α] [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

theorem Finset.factorization_lcm {ι : Type u_1} {f : ι → ℕ} {s : Finset ι} (hf : ∀ k ∈ s, f k ≠ 0) (p : ℕ) : (s.lcm f).factorization p = s.sup fun (a : ι) => (f a).factorization p

An analogue of Nat.factorization_lcm for Finset.lcm.

theorem Finset.Rat.den_sum_dvd_lcm_den {ι : Type u_3} (s : Finset ι) (f : ι → ℚ) : (∑ i ∈ s, f i).den ∣ s.lcm fun (i : ι) => (f i).den

theorem Finset.Rat.den_sum_dvd_prod_den {ι : Type u_3} (s : Finset ι) (f : ι → ℚ) : (∑ i ∈ s, f i).den ∣ ∏ i ∈ s, (f i).den

theorem Finset.Rat.den_prod_dvd_prod_den {ι : Type u_3} (s : Finset ι) (f : ι → ℚ) : (∏ i ∈ s, f i).den ∣ ∏ i ∈ s, (f i).den