English
The finite product (pi) of finitely generated subgroups in a finite index family is finitely generated.
Русский
Конечный произведение FG-подгрупп по индексу i в семействе. FG.
LaTeX
$$$\forall {i \in ι}, (P i).FG \to (\mathrm{pi} \; Set.univ \; P).FG$$$
Lean4
/-- Finite product of finitely generated subgroups is finitely generated. -/
@[to_additive /-- Finite product of finitely generated additive subgroups is finitely generated. -/
]
theorem pi {ι : Type*} [Finite ι] {G : ι → Type*} [∀ i, Group (G i)] {P : ∀ i, Subgroup (G i)} (hP : ∀ i, (P i).FG) :
(pi Set.univ P).FG := by
simp_rw [fg_iff_submonoid_fg] at *
exact .pi hP
