one_ascFactorial — Mathlib

English

Let k be a natural number. The ascending factorial with starting value 1 equals the ordinary factorial: (1)^{̅{k}} = k!.

Русский

Пусть k — натуральное число. Возрастающий факториал с начальным значением 1 равен обычному факториалу: (1)^{\overline{k}} = k!.

LaTeX

$$$$\forall k \in \mathbb{N}, (1)^{\overline{k}} = k!$$$$

Lean4

@[simp]
theorem one_ascFactorial : ∀ (k : ℕ), (1 : ℕ).ascFactorial k = k.factorial
  | 0 => ascFactorial_zero 1
  | (k + 1) => by rw [ascFactorial_succ, one_ascFactorial k, Nat.add_comm, factorial_succ]

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