choose_lt_pow_div — Mathlib

English

For hn ≠ 0 and hk ≥ 2, (n choose k) < (n^k)/k! when viewed in a semifield α.

Русский

При hn ≠ 0 и hk ≥ 2 выполняется C(n,k) < n^k / k! в полях α.

LaTeX

$$$$ (n\choose k) < (n^k) / k! $$$$

Lean4

theorem choose_lt_pow_div (hn : n ≠ 0) (hk : 2 ≤ k) : (n.choose k : α) < (n ^ k : α) / k ! :=
  by
  rw [lt_div_iff₀' (mod_cast k.factorial_pos)]
  norm_cast
  rw [← Nat.descFactorial_eq_factorial_mul_choose]
  exact descFactorial_lt_pow hn hk

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