English
If you start with a prime multiset v and take its product, then factor it back, you recover v.
Русский
Начавшие с мультимножества простых v и взяв произведение, затем разложив фактор Multiset обратно, получаем то же v.
LaTeX
$$$ v.prod.factorMultiset = v $$$
Lean4
/-- If we start with a multiset of primes, take the product and
then factor it, we get back the original multiset. -/
theorem factorMultiset_prod (v : PrimeMultiset) : v.prod.factorMultiset = v :=
by
apply PrimeMultiset.coeNat_injective
rw [v.prod.coeNat_factorMultiset, PrimeMultiset.coe_prod]
rcases v with ⟨l⟩
dsimp [PrimeMultiset.toNatMultiset]
let l' := l.map ((↑) : Nat.Primes → ℕ)
have (p : ℕ) (hp : p ∈ l') : p.Prime :=
by
simp only [List.map_subtype, List.map_id_fun', id_eq, List.mem_unattach, l'] at hp
obtain ⟨hp', -⟩ := hp
exact hp'
exact Multiset.coe_eq_coe.mpr (@Nat.primeFactorsList_unique _ l' rfl this).symm
