prod_divisorsAntidiagonal — Mathlib

English

For any M a commutative monoid and f: ℕ × ℕ → M, the product over i in n.divisorsAntidiagonal of f(i.1,i.2) equals the product over i in n.divisors of f(i, n/i).

Русский

Для любой композиционной моноиды M и функции f: ℕ×ℕ → M произведение по i в n.divisorsAntidiagonal f(i.1,i.2) равно произведению по i в n.divisors f(i,n/i).

LaTeX

$$$\displaystyle \prod_{i \in n.\mathrm{divisorsAntidiagonal}} f(i.1,i.2) = \prod_{i \in n.\mathrm{divisors}} f(i, n/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 i (n / i) :=
  by
  rw [← map_div_right_divisors, Finset.prod_map]
  rfl

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