English
If a multiset of natural numbers consists only of primes, it can be converted into a PrimeMultiset by pairing each element with its primality witness.
Русский
Если мультимножество натуральных чисел состоит только из простых, оно может быть преобразовано в PrimeMultiset путём связывания каждого элемента с доказательством простоты.
LaTeX
$$$ \\operatorname{ofNatMultiset}(v,h) = \\operatorname{Multiset.pmap}(\\lambda p\\, hp. \\langle p, hp \\rangle)\\ v\\ h $$$
Lean4
/-- If a `Multiset ℕ` consists only of primes, it can be recast as a `PrimeMultiset`. -/
def ofNatMultiset (v : Multiset ℕ) (h : ∀ p : ℕ, p ∈ v → p.Prime) : PrimeMultiset :=
@Multiset.pmap ℕ Nat.Primes Nat.Prime (fun p hp => ⟨p, hp⟩) v h
