factorialBinarySplitting_eq_factorial

English

The standard factorial equals the binary-splitting factorial: factorial = factorialBinarySplitting.

Русский

Стандартный факториал равен факториалу через бинарное разбиение: factorial = factorialBinarySplitting.

LaTeX

$$@factorial = @factorialBinarySplitting$$

Lean4

@[csimp]
theorem factorialBinarySplitting_eq_factorial : @factorial = @factorialBinarySplitting :=
  by
  ext n
  by_cases h : n = 0
  · simp [h, factorialBinarySplitting]
  · rw [factorialBinarySplitting, ← factorialBinarySplitting.factorial_mul_prodRange 0 n (by grind)]
    simp [h]

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