factorization_choose_eq_zero_of_lt

English

If n < p, then (n choose k).factorization p = 0 for all k.

Русский

Если n < p, то (n над k).factorization p = 0 для любого k.

LaTeX

$$$ (n \\choose k).factorization p = 0 \\quad\\text{если } n < p. $$$

Lean4

theorem factorization_choose_eq_zero_of_lt (h : n < p) : (choose n k).factorization p = 0 :=
  by
  by_cases hnk : n < k; · simp [choose_eq_zero_of_lt hnk]
  rw [choose_eq_factorial_div_factorial (le_of_not_gt hnk),
    factorization_div (factorial_mul_factorial_dvd_factorial (le_of_not_gt hnk)), Finsupp.coe_tsub, Pi.sub_apply,
    factorization_factorial_eq_zero_of_lt h, zero_tsub]

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