sum_Ico_reflect — Mathlib

English

A factorial identity via Ico: ∏_{x∈Ico(1,n+1)} x equals n!, in another presentation.

Русский

Факториал через Ico: произведение по Ico(1,n+1) равно n!, другой вид записи.

LaTeX

$$$$ \\displaystyle \\prod_{x \\in \\mathrm{Ico}(1,n+1)} x = n!. $$$$

Lean4

theorem sum_Ico_reflect {δ : Type*} [AddCommMonoid δ] (f : ℕ → δ) (k : ℕ) {m n : ℕ} (h : m ≤ n + 1) :
    (∑ j ∈ Ico k m, f (n - j)) = ∑ j ∈ Ico (n + 1 - m) (n + 1 - k), f j :=
  @prod_Ico_reflect (Multiplicative δ) _ f k m n h

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