factorial_mul_factorial_dvd_factorial

Mathlib.Data.Nat.Choose.Basic

URI: https://scilib.ai/kg/mathlib#Nat.factorial_mul_factorial_dvd_factorial

← MathLib Explorer

English

If k ≤ n, then k! (n-k)! divides n!.

Русский

Если k ≤ n, то k! (n-k)! делит n!.

LaTeX

$$$\\\\forall {n k}, k \\\\le n \\\\Rightarrow k! (n-k)! \\\\mid n!$$$

Lean4

theorem factorial_mul_factorial_dvd_factorial {n k : ℕ} (hk : k ≤ n) : k ! * (n - k)! ∣ n ! := by
  rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]; exact Nat.dvd_mul_left _ _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru