factorial_dvd_factorial

Mathlib.Data.Nat.Factorial.Basic

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

← MathLib Explorer

English

If m ≤ n, then m! divides n!.

Русский

Если m ≤ n, то m! делится на n!.

LaTeX

$$$m \le n \Rightarrow m! \mid n!$$$

Lean4

@[gcongr]
theorem factorial_dvd_factorial {m n} (h : m ≤ n) : m ! ∣ n ! := by
  induction h with
  | refl => exact Nat.dvd_refl _
  | step _ ih => exact Nat.dvd_trans ih (Nat.dvd_mul_left _ _)

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

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

Разделы

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

Аффилиация

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