prod_antidiagonal_eq_prod_range_succ_mk

English

For a function f: ℕ×ℕ → M and n ∈ ℕ,

Русский

Для функции f: ℕ×ℕ → M и данного n:

LaTeX

$$$$ \\prod_{ij ∈ \\mathrm{antidiagonal}(n)} f(ij) = \\prod_{k ∈ \\mathrm{range}(n+1)} f(k, n - k). $$$$

Lean4

@[to_additive]
theorem prod_antidiagonal_eq_prod_range_succ_mk {M : Type*} [CommMonoid M] (f : ℕ × ℕ → M) (n : ℕ) :
    ∏ ij ∈ antidiagonal n, f ij = ∏ k ∈ range n.succ, f (k, n - k) :=
  Finset.prod_map (range n.succ) ⟨fun i ↦ (i, n - i), fun _ _ h ↦ (Prod.mk.inj h).1⟩ f

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