prod_properDivisors_prime_pow — Mathlib

English

Let p be prime and k a natural number. For any f, the product over x in (p^k).properDivisors of f(x) equals the product over x in range(k) of f(p^x).

Русский

Пусть p простое, k натурал. Для функции f произведение по x из (p^k).properDivisors f(x) равно произведению по x от 0 до k-1 f(p^x).

LaTeX

$$$\displaystyle \prod_{x \in (p^k).properDivisors} f(x) = \prod_{x \in \mathrm{range}(k)} f(p^x).$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_properDivisors_prime_pow {α : Type*} [CommMonoid α] {k p : ℕ} {f : ℕ → α} (h : p.Prime) :
    (∏ x ∈ (p ^ k).properDivisors, f x) = ∏ x ∈ range k, f (p ^ x) := by simp [h, properDivisors_prime_pow]

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