prod_antidiagonal_swap — Mathlib

English

The product over antidiagonal n of f(p.swap) equals the product over antidiagonal n of f(p).

Русский

Произведение по антидиагонали n от f(p.swap) равно произведению по anti-diagonal n от f(p).

LaTeX

$$$$ \\prod_{p \\in \\mathrm{antidiagonal}(n)} f(p.swap) = \\prod_{p \\in \\mathrm{antidiagonal}(n)} f(p). $$$$

Lean4

@[to_additive]
theorem prod_antidiagonal_swap {n : ℕ} {f : ℕ × ℕ → M} : ∏ p ∈ antidiagonal n, f p.swap = ∏ p ∈ antidiagonal n, f p :=
  by
  conv_lhs => rw [← map_swap_antidiagonal, Finset.prod_map]
  rfl

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