Finding a home for lemmas about Finset.lcm/Finset.prod

Stream: mathlib4

[Snir Broshi]

I'm not sure where to place these lemmas, and #find_home doesn't give any sensible output (it might be confused since Mathlib moved to the module system):

Finset.lcm/Finset.prod lemmas

import Mathlib

theorem Finset.lcm_dvd_prod {α β : Type*} [CancelCommMonoidWithZero β] [NormalizedGCDMonoid β]
    (s : Finset α) (f : α → β) : s.lcm f ∣ s.prod f :=
  lcm_dvd fun _ ↦ dvd_prod_of_mem _

theorem Finset.associated_lcm_prod {α β : Type*} [CancelCommMonoidWithZero β]
    [NormalizedGCDMonoid β] (s : Finset α) (f : α → β) (h : Set.Pairwise s <| IsRelPrime.onFun f) :
    Associated (s.lcm f) (s.prod f) :=
  associated_of_dvd_dvd (s.lcm_dvd_prod f) (s.prod_dvd_of_isRelPrime h fun _ ↦ dvd_lcm)

theorem Finset.lcm_eq_prod {α : Type*} (s : Finset α) (f : α → ℕ)
    (h : Set.Pairwise s <| Nat.Coprime.onFun f) : s.lcm f = s.prod f := by
  have : Nat.Coprime = IsRelPrime := funext₂ fun _ _ ↦ propext Nat.coprime_iff_isRelPrime
  exact (associated_lcm_prod s f <| this ▸ h).eq_of_normalized (normalize_eq _) (normalize_eq _)

[Snir Broshi]

Where should I place these? The relevant files are:

• Mathlib.Algebra.GCDMonoid.Finset: defines Finset.lcm and contains Finset.lcm_dvd/Finset.dvd_lcm
• Mathlib.RingTheory.Coprime.Lemmas: contains Finset.prod_dvd_of_isRelPrime
• Mathlib.Algebra.BigOperators.Group.Finset.Piecewise: contains Finset.dvd_prod_of_mem
• Mathlib.Algebra.GroupWithZero.Associated: defines Associated and contains associated_of_dvd_dvd
• Mathlib.Data.Nat.GCD.Basic: contains Nat.coprime_iff_isRelPrime
• Mathlib.Algebra.GCDMonoid.Nat: contains an instance for NormalizedGCDMonoid ℕ

The min imports for them is:

import Mathlib.Algebra.GCDMonoid.Finset
import Mathlib.Algebra.GCDMonoid.Nat
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.RingTheory.Coprime.Lemmas

There are ~1000 files in mathlib that include all of these requirements, but none of them are very related to these lemmas.

[Snir Broshi]

So the question is: should I create a new file for these or can I add imports in an existing file?
The modules I mentioned seem to be pretty popular so I'm worried about adding imports.

[Snir Broshi]

Does anyone have ideas? Otherwise, can an admin please move this to the mathlib channel?

[Notification Bot]

This topic was moved here from #new members > Finding a home for lemmas about Finset.lcm/Finset.prod by Kevin Buzzard.