prod_divisors — Mathlib

English

Let p be prime and f: ℕ → α. Then the product over all divisors of p of f(x) equals f(p) times f(1).

Русский

Пусть p — простое число и f: ℕ → α. Тогда произведение f(x) по всем делителям p равно f(p)·f(1).

LaTeX

$$$\displaystyle \prod_{x \in p.divisors} f(x) = f(p) \cdot f(1).$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_divisors {α : Type*} [CommMonoid α] {p : ℕ} {f : ℕ → α} (h : p.Prime) :
    ∏ x ∈ p.divisors, f x = f p * f 1 := by rw [← cons_self_properDivisors h.ne_zero, prod_cons, h.prod_properDivisors]

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