mul_factorial_pred

Mathlib.Data.Nat.Factorial.Basic

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

English

If n ≠ 0, then n! = n · (n−1)!.

Русский

Если n ≠ 0, то n! = n · (n−1)!.

LaTeX

$$$n \neq 0 \Rightarrow n! = n \cdot (n-1)!$$$

Lean4

theorem mul_factorial_pred (hn : n ≠ 0) : n * (n - 1)! = n ! :=
  Nat.sub_add_cancel (one_le_iff_ne_zero.mpr hn) ▸ rfl

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

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

Разделы

Аффилиация

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