factorMultiset_ofPrime — Mathlib

English

Factoring a prime yields the corresponding one-element multiset.

Русский

Разложение простого числа дает одноэлементное мультимножество, содержащее этот простой.

LaTeX

$$$ (p : \\mathbb{N}^+).\\operatorname{factorMultiset} = \\operatorname{PrimeMultiset.ofPrime}(p) $$$

Lean4

/-- Factoring a prime gives the corresponding one-element multiset. -/
theorem factorMultiset_ofPrime (p : Nat.Primes) : (p : ℕ+).factorMultiset = PrimeMultiset.ofPrime p :=
  by
  apply factorMultisetEquiv.symm.injective
  change (p : ℕ+).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod
  rw [(p : ℕ+).prod_factorMultiset, PrimeMultiset.prod_ofPrime]

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