Fundamental_Theorem_of_Arithmetic
Provedfactorizationfundamental-theoremsprime-decompositionsprime-numbersproofwiki
Every integer n > 1 can be expressed as a product of primes.
Preamble
import Mathlib.Data.Nat.Prime.Basic import Mathlib.Tactic
Formal statement
theorem Fundamental_Theorem_of_Arithmetic (n : ℕ) (hn : n > 1) : ∃ l : List ℕ, (∀ p ∈ l, Nat.Prime p) ∧ l.prod = n := by sorry
Source