prod_antidiagonal_swap — Mathlib

English

Swapping the coordinates in the antidiagonal product does not change the product.

Русский

Перестановка координат в произведении антидиагонали не изменяет значение произведения.

LaTeX

$$$\\prod p \\in \\operatorname{antidiagonal} n\\, f(p.1,p.2) = \\prod p \\in \\operatorname{antidiagonal} n\\, f(p.2,p.1)$$$

Lean4

@[to_additive]
theorem prod_antidiagonal_swap {M : Type*} [CommMonoid M] (n : α →₀ ℕ) (f : (α →₀ ℕ) → (α →₀ ℕ) → M) :
    ∏ p ∈ antidiagonal n, f p.1 p.2 = ∏ p ∈ antidiagonal n, f p.2 p.1 :=
  prod_equiv (Equiv.prodComm _ _) (by simp [add_comm]) (by simp)

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