factorization_prod_pow_eq_self — Mathlib

English

The product of p^{v_p(n)} over primes p equals n; i.e., n = ∏_{p prime} p^{v_p(n)}.

Русский

Произведение p^{v_p(n)} по всем простым p даёт n; то есть n = ∏_{p prime} p^{v_p(n)}.

LaTeX

$$$ n = \prod_{p \text{ prime}} p^{n.factorization p} $$$

Lean4

@[simp]
theorem factorization_prod_pow_eq_self {n : ℕ} (hn : n ≠ 0) : n.factorization.prod (· ^ ·) = n :=
  by
  rw [factorization_eq_primeFactorsList_multiset n]
  simp only [← prod_toMultiset, Multiset.prod_coe, Multiset.toFinsupp_toMultiset]
  exact prod_primeFactorsList hn

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