factorizationEquiv_inv_apply — Mathlib

English

Under the inverse correspondence, the image equals the product ∏ p p^{f(p)}.

Русский

Под обратным соответствием образ равен произведению \prod_p p^{f(p)}.

LaTeX

$$$ (\text{factorizationEquiv}^{-1} \langle f, hf \rangle).1 = \prod_p p^{f(p)} $$$

Lean4

theorem factorizationEquiv_inv_apply {f : ℕ →₀ ℕ} (hf : ∀ p ∈ f.support, Prime p) :
    (factorizationEquiv.symm ⟨f, hf⟩).1 = f.prod (· ^ ·) :=
  rfl

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