factorial_mul_prodRange — Mathlib

English

If lo < hi, then lo! · prodRange (lo+1) (hi+1) = hi!, i.e., successively extending the product by one step multiplies the factorial accordingly.

Русский

Если lo < hi, то lo! · prodRange (lo+1) (hi+1) = hi!, то есть факториал увеличивается факториальным способом при добавлении новых факторов.

LaTeX

$$lo! · prodRange (lo+1) (hi+1) = hi! \\\\ (lo < hi)$$

Lean4

theorem factorial_mul_prodRange (lo hi : Nat) (h : lo < hi) : lo ! * prodRange (lo + 1) (hi + 1) = hi ! :=
  by
  rw [prodRange]
  split
  · grind [factorial_succ]
  · dsimp only
    rw [← Nat.mul_assoc]
    simp_rw [show (lo + 1 + (hi + 1)) / 2 = (lo + hi) / 2 + 1 by grind]
    rw [factorial_mul_prodRange, factorial_mul_prodRange]
    all_goals grind

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