Integer_is_Expressible_as_Product_of_Primes

import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Tactic

theorem Integer_is_Expressible_as_Product_of_Primes (n : ℕ) (hn : n > 1) : ∃ l : List ℕ, (∀ p ∈ l, Nat.Prime p) ∧ l.prod = n := by sorry