lean_workbook_plus_37758

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that $x_1! \cdot x_2! \cdot ... \cdot x_k!~|~(x_1+x_2+...+x_k)!$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37758 (x : ℕ → ℕ) (k : ℕ) :
  ∏ i in Finset.range k, (x i)! ∣ (∑ i in Finset.range k, x i)!   :=  by sorry

Source