English
The lower central series of a product equals the product of the lower central series of the factors.
Русский
Нижняя центральная последовательность произведения равна произведению нижних центральных последовательностей факторов.
LaTeX
$$$\\lowerCentralSeries (G_1 \\times G_2)\\, n = (\\lowerCentralSeries G_1\\, n) \\cdot (\\lowerCentralSeries G_2\\, n)$$$
Lean4
theorem lowerCentralSeries_prod (n : ℕ) :
lowerCentralSeries (G₁ × G₂) n = (lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n) := by
induction n with
| zero => simp
| succ n ih =>
calc
lowerCentralSeries (G₁ × G₂) n.succ = ⁅lowerCentralSeries (G₁ × G₂) n, ⊤⁆ := rfl
_ = ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), ⊤⁆ := by rw [ih]
_ = ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), (⊤ : Subgroup G₁).prod ⊤⁆ := by simp
_ = ⁅lowerCentralSeries G₁ n, (⊤ : Subgroup G₁)⁆.prod ⁅lowerCentralSeries G₂ n, ⊤⁆ :=
(commutator_prod_prod _ _ _ _)
_ = (lowerCentralSeries G₁ n.succ).prod (lowerCentralSeries G₂ n.succ) := rfl
