English
Direct products of torsion-free groups are torsion-free.
Русский
Прямые произведения безторсионных групп тоже безторсионны.
LaTeX
$$$\text{IsTorsionFree } G_i \quad\text{for all } i \\Rightarrow\\ IsTorsionFree (\prod_i G_i)$$$
Lean4
/-- Direct products of torsion free groups are torsion free. -/
@[to_additive (attr := deprecated Pi.instIsMulTorsionFree (since := "2025-04-23")) AddMonoid.IsTorsionFree.prod /--
Direct products of additive torsion free groups are torsion free. -/
]
theorem prod {η : Type*} {Gs : η → Type*} [∀ i, Group (Gs i)] (tfGs : ∀ i, IsTorsionFree (Gs i)) :
IsTorsionFree <| ∀ i, Gs i := fun w hne h =>
hne <| funext fun i => Classical.not_not.mp <| mt (tfGs i (w i)) <| Classical.not_not.mpr <| h.apply i
