prod_antidiagonal_subst

Mathlib.Algebra.BigOperators.NatAntidiagonal

URI: https://scilib.ai/kg/mathlib#Finset.Nat.prod_antidiagonal_subst

← MathLib Explorer

English

Let f: ℕ×ℕ → ℕ → M. Then

Русский

Пусть f: ℕ×ℕ → ℕ → M. Тогда:

LaTeX

$$$$ \\prod_{p \\in \\mathrm{antidiagonal}(n)} f(p,n) = \\prod_{p \\in \\mathrm{antidiagonal}(n)} f(p_1 + p_2). $$$$

Lean4

@[to_additive]
theorem prod_antidiagonal_subst {n : ℕ} {f : ℕ × ℕ → ℕ → M} :
    ∏ p ∈ antidiagonal n, f p n = ∏ p ∈ antidiagonal n, f p (p.1 + p.2) :=
  prod_congr rfl fun p hp ↦ by rw [mem_antidiagonal.mp hp]

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

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

Разделы

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

Аффилиация

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