prod_primeFactors_prod_factorization

English

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

Русский

Произведение по простым факторам равно произведению по факторизации, считая экспоненты для каждого простого.

LaTeX

$$$ \prod_{p \in n.primeFactors} f(p) = n.factorization.prod (\lambda p \; \_ \mapsto f(p)) $$$

Lean4

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

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