Lean-Workbook Syntax 37758: Product of factorials divides factorial of the sum

For any finite list of natural numbers $x_0,\ldots,x_{k-1}$, $\prod_{i=0}^{k-1}x_i!\mid\bigl(\sum_{i=0}^{k-1}x_i\bigr)!$.

Source: Lean-Workbook row lean_workbook_plus_37758 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.