English
If a family of elements I(i) is pairwise coprime over a finite index set s, then the infimum over i∈s of span({I(i)}) equals the span of the product ∏_{i∈s} I(i).
Русский
Если элементы I(i) попарно coprime по конечному индексу s, то наименьшее (сколь угодно мелкое) значение пересечения спанов равно спану произведения ∏ I(i).
LaTeX
$$$\inf_{i\in s} \operatorname{span}\{I(i)\} = \operatorname{span}\left(\prod_{i\in s} I(i)\right)$$$
Lean4
theorem finset_inf_span_singleton {ι : Type*} (s : Finset ι) (I : ι → R) (hI : Set.Pairwise (↑s) (IsCoprime on I)) :
(s.inf fun i => Ideal.span ({I i} : Set R)) = Ideal.span {∏ i ∈ s, I i} :=
by
ext x
simp only [Submodule.mem_finsetInf, Ideal.mem_span_singleton]
exact ⟨Finset.prod_dvd_of_coprime hI, fun h i hi => (Finset.dvd_prod_of_mem _ hi).trans h⟩
