eq_factorization_iff — Mathlib

English

For nonzero n and for any f with primes in its support, f = n.factorization iff the product over primes p of p^{f(p)} equals n.

Русский

Для нес нулевого n и любого f со сведениями о простых, f = n.factorization тогда и только тогда, когда произведение над p^{f(p)} равно n.

LaTeX

$$$ f = n.factorization \iff \prod_p p^{f(p)} = n $$$

Lean4

theorem eq_factorization_iff {n : ℕ} {f : ℕ →₀ ℕ} (hn : n ≠ 0) (hf : ∀ p ∈ f.support, Prime p) :
    f = n.factorization ↔ f.prod (· ^ ·) = n :=
  ⟨fun h => by rw [h, factorization_prod_pow_eq_self hn], fun h => by rw [← h, prod_pow_factorization_eq_self hf]⟩

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