prod_diag — Mathlib

English

For a finite set s and a function f on pairs, the product over the diagonal of s equals the product over s of f(i,i).

Русский

Для конечного множества s и функции f на попарных элементах имеет место равенство произведения по диагонали равному произведению по i∈s от f(i,i).

LaTeX

$$$\prod_{i\in s.diag} f(i) = \prod_{i\in s} f(i,i)$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_diag [DecidableEq ι] (s : Finset ι) (f : ι × ι → M) : ∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i) := by
  apply prod_nbij' Prod.fst (fun i ↦ (i, i)) <;> simp

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