prod_factorial_dvd_factorial_sum — Mathlib

English

For any finite set s and function f, the product ∏_{i∈s} (f(i))! divides (∑_{i∈s} f(i))!.

Русский

Для любого конечного множества s и функции f произведение ∏_{i∈s} (f(i))! делит (∑_{i∈s} f(i))!.

LaTeX

$$∏_{i∈s} (f(i))! ∣ (∑_{i∈s} f(i))!$$

Lean4

theorem prod_factorial_dvd_factorial_sum : (∏ i ∈ s, (f i)!) ∣ (∑ i ∈ s, f i)! := by
  induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s has ih =>
    rw [prod_cons, Finset.sum_cons]
    exact (mul_dvd_mul_left _ ih).trans (Nat.factorial_mul_factorial_dvd_factorial_add _ _)

Похожие утверждения