prod_divisors_prime_pow — Mathlib

English

Let p be prime. Then the product over all divisors d of p^k of f(d) equals the product over x from 0 to k of f(p^x).

Русский

Пусть p простое. Тогда произведение f(d) по всем делителям p^k равно произведению по x от 0 до k от f(p^x).

LaTeX

$$$\displaystyle \prod_{d \mid p^k} f(d) = \prod_{x=0}^{k} f(p^x).$$$

Lean4

@[to_additive (attr := simp) sum_divisors_prime_pow]
theorem prod_divisors_prime_pow {α : Type*} [CommMonoid α] {k p : ℕ} {f : ℕ → α} (h : p.Prime) :
    (∏ x ∈ (p ^ k).divisors, f x) = ∏ x ∈ range (k + 1), f (p ^ x) := by simp [h, divisors_prime_pow]

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