English
For a finite type with a commutative monoid M and a function f: α → α → M, the double product over i of the inner product over j in the set {i}ᶜ of f(j,i) equals the corresponding off-diagonal product; i.e., a symmetry identity relating diagonal complement sets.
Русский
Для конечного типа с коммутативным монадом M и функцией f: α → α → M, имеет место тождество, связывающее двойное произведение по i и по j в множестве {i}ᶜ и соответствующее 'вне диагонали' произведение.
LaTeX
$$$ \prod_{i} \prod_{j \in \{i\}^{c}} f(j,i) = \prod_{i} \prod_{j \in \mathrm{Ioi}(i)\cup \mathrm{Iio}(i)} f(j,i) $$$
Lean4
@[to_additive]
theorem prod_prod_Ioi_mul_eq_prod_prod_off_diag (f : α → α → M) :
∏ i, ∏ j ∈ Ioi i, f j i * f i j = ∏ i, ∏ j ∈ { i }ᶜ, f j i :=
by
simp_rw [← Ioi_disjUnion_Iio, prod_disjUnion, prod_mul_distrib]
congr 1
rw [prod_sigma', prod_sigma']
refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_ <;> simp
