prod_properDivisors — Mathlib

English

If p is prime and f is a function from natural numbers to a commutative monoid, then the product over all proper divisors of p of f(x) equals f(1).

Русский

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

LaTeX

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

Lean4

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

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