English
Let I_i be ideals in a ring R indexed by a finite set s. If each I_i is FG and each R/(I_i) is finite, then R/(∏_{i∈s} I_i) is finite.
Русский
Пусть I_i — идеалы кольца R, индексируемые конечным множеством s. Если каждый I_i имеет конечный индекс и каждый фактор кольца R/I_i конечен, то фактор по произведению ∏ I_i тоже конечен.
LaTeX
$$$$\text{Finite}\left( R / \left(\prod_{i\in s} I_i\right)\right).$$$$
Lean4
theorem finite_quotient_prod {ι : Type*} (I : ι → Ideal R) (s : Finset ι) (hI : ∀ i ∈ s, (I i).FG)
(hI' : ∀ i ∈ s, Finite (R ⧸ I i)) : Finite (R ⧸ (∏ i ∈ s, I i)) := by
classical
induction s using Finset.induction_on with
| empty => simp only [Finset.prod_empty, one_eq_top]; infer_instance
| insert a s has IH =>
rw [Finset.prod_insert has, mul_comm]
have := hI' a (by simp)
have := IH (fun i hi ↦ hI _ (by simp [hi])) (fun i hi ↦ hI' _ (by simp [hi]))
exact Submodule.finite_quotient_smul _ (hI a (by simp))
