prod_factorMultiset — Mathlib

English

The multiset of primes corresponding to a prime multiset equals the original multiset of naturals when viewed as PNats.

Русский

Мультимножество простых, полученное из PNats, отображается обратно в исходное мультимножество простых.

LaTeX

$$$ (v : \\operatorname{Multiset}\\mathbb{N}_{+}) (h) : (\\operatorname{ofPNatMultiset}(v,h) : \\operatorname{Multiset}\\mathbb{N}_{+}) = v $$$

Lean4

/-- The product of the factors is the original number -/
theorem prod_factorMultiset (n : ℕ+) : (factorMultiset n).prod = n :=
  eq <| by
    dsimp [factorMultiset]
    rw [PrimeMultiset.prod_ofNatList]
    exact Nat.prod_primeFactorsList n.ne_zero

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