English
If l is a list of primes whose product equals n, then l is a permutation of the standard prime factors list of n.
Русский
Если список l состоит из простых чисел и произведение его элементов равно n, то l является перестановкой стандартного списка простых делителей n.
LaTeX
$$prod(l) = n \rightarrow (\forall p \in l, Prime(p)) \rightarrow l ~ primeFactorsList(n)$$
Lean4
/-- **Fundamental theorem of arithmetic** -/
theorem primeFactorsList_unique {n : ℕ} {l : List ℕ} (h₁ : prod l = n) (h₂ : ∀ p ∈ l, Prime p) :
l ~ primeFactorsList n := by
refine perm_of_prod_eq_prod ?_ ?_ ?_
· rw [h₁]
refine (prod_primeFactorsList ?_).symm
rintro rfl
rw [prod_eq_zero_iff] at h₁
exact Prime.ne_zero (h₂ 0 h₁) rfl
· simp_rw [← prime_iff]
exact h₂
· simp_rw [← prime_iff]
exact fun p => prime_of_mem_primeFactorsList
