factorMultisetEquiv — Mathlib

English

Positive integers are in bijection with prime multisets via factorMultiset and prod.

Русский

Положительные целые числа образуют биекцию с простыми мультимножестами через factorMultiset и prod.

LaTeX

$$$ \\text{Equiv } \\mathbb{N}_{+} \\;\\cong\\; \\text{PrimeMultiset} $$

Lean4

/-- Positive integers biject with multisets of primes. -/
def factorMultisetEquiv : ℕ+ ≃ PrimeMultiset where
  toFun := factorMultiset
  invFun := PrimeMultiset.prod
  left_inv := prod_factorMultiset
  right_inv := PrimeMultiset.factorMultiset_prod

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