English
For any PrimeMultiset v, the multiset of naturals obtained by viewing elements as natural numbers equals the underlying nat-multiset.
Русский
Для любого PrimeMultiset v мульти-множество натуральных чисел, получаемое путём рассмотрения элементов как натуральных чисел, совпадает с исходным мульти-множеством натуральных чисел.
LaTeX
$$$ ((v : \\operatorname{Multiset}\\mathbb{N}_{+}) : \\operatorname{Multiset}\\mathbb{N}) = (v : \\operatorname{Multiset}\\mathbb{N}) $$$
Lean4
theorem coePNat_nat (v : PrimeMultiset) : ((v : Multiset ℕ+) : Multiset ℕ) = (v : Multiset ℕ) :=
by
change (v.map ((↑) : Nat.Primes → ℕ+)).map Subtype.val = v.map Subtype.val
rw [Multiset.map_map]
rfl
