prod_factorization_eq_prod_primeFactors

English

A product over n.factorization can be written as a product over n.primeFactors; i.e., the product across factorization equals the product across prime factors with exponents.

Русский

Произведение по факторизации равносильно произведению по простым множителям с учётом степеней (экспонент).

LaTeX

$$$ \left(n.factorization\right).prod f = \prod_{p \in n.primeFactors} f(p)^{n.factorization(p)} $$$

Lean4

/-- A product over `n.factorization` can be written as a product over `n.primeFactors`; -/
theorem prod_factorization_eq_prod_primeFactors {β : Type*} [CommMonoid β] (f : ℕ → ℕ → β) :
    n.factorization.prod f = ∏ p ∈ n.primeFactors, f p (n.factorization p) :=
  rfl

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