English
Let R be a commutative ring and ι a finite index set with a family I: ι → ℕ whose elements are pairwise coprime. Then the intersection of the principal ideals generated by I(i) in R equals the principal ideal generated by the product of all I(i) (viewed in R): ⨅ i (I(i)R) = (∏ i I(i))R.
Русский
Пусть R — коммутативное кольцо и ι — конечный множество индексов с семейством чисел I(i) ∈ ℕ, попарно взаимно простых. Тогда пересечение порожденных ими основных идеалов в R равно основному идеалу, порожденному произведением всех I(i): ∏ I(i)R = (∏ i I(i))R.
LaTeX
$$$ \bigcap_{i \in \iota} (I(i)R) = \left( \prod_{i \in \iota} I(i) \right) R. $$$
Lean4
theorem iInf_span_singleton_natCast {R : Type*} [CommRing R] {ι : Type*} [Fintype ι] {I : ι → ℕ}
(hI : Pairwise fun i j => (I i).Coprime (I j)) : ⨅ (i : ι), span {(I i : R)} = span {((∏ i : ι, I i : ℕ) : R)} :=
by
rw [iInf_span_singleton, Nat.cast_prod]
exact fun i j h ↦ (hI h).cast
