English
For any M a commutative monoid and f: ℕ → ℕ → M, the product over i ∈ n.divisorsAntidiagonal of f i.1 i.2 equals the product over i ∈ n.divisors of f (n / i) i.
Русский
Для любой коммутативной моноиды M и функции f: ℕ × ℕ → M, произведение по i∈n.divisorsAntidiagonal f i.1 i.2 равно произведению по i∈n.divisors f (n/i) i.
LaTeX
$$$\displaystyle \prod_{i \in n.\mathrm{divisorsAntidiagonal}} f(i.1,i.2) = \prod_{i \in n.\mathrm{divisors}} f(n/i,i).$$$
Lean4
@[to_additive]
theorem prod_divisorsAntidiagonal' {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} :
∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i :=
by
rw [← map_swap_divisorsAntidiagonal, Finset.prod_map]
exact prod_divisorsAntidiagonal fun i j => f j i
