sum_range_reflect

Mathlib.Algebra.BigOperators.Intervals

URI: https://scilib.ai/kg/mathlib#Finset.sum_range_reflect

← MathLib Explorer

English

Gauss summation disguised as a product: the product ∏_{x∈Ico(1,n+1)} x equals n!.

Русский

Произведение по Ico(1,n+1) равно факториалу n!.

LaTeX

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

Lean4

theorem sum_range_reflect {δ : Type*} [AddCommMonoid δ] (f : ℕ → δ) (n : ℕ) :
    (∑ j ∈ range n, f (n - 1 - j)) = ∑ j ∈ range n, f j :=
  @prod_range_reflect (Multiplicative δ) _ f n

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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