Fundamental theorem of arithmetic --- uniqueness

Proved

FundamentalTheoremOfArithmetic.fta_uniqueness

by Mayank Kumar · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryprime-numbers

This is the uniqueness half of the Fundamental Theorem of Arithmetic (Apostol, Introduction to Analytic Number Theory, 1976, Theorem 1.10): any two multisets of primes with the same product are equal.

\left(\forall p \in l_1,\ p \text{ prime}\right) \wedge \left(\forall p \in l_2,\ p \text{ prime}\right) \wedge \prod_{p \in l_1} p = n = \prod_{p \in l_2} p \ \implies\ l_1 = l_2.

The conclusion $l_1 = l_2$ is equality of multisets: the same primes occur in $l_1$ and $l_2$ , with exactly the same multiplicities, regardless of the order in which they are listed. Combined with the existence milestone, this yields the mission's goal theorem, that every nonzero $n$ has exactly one such multiset.

This lemma is what makes "the" prime factorization of an integer a well-defined object, rather than merely one possible representation among several.

Formalization Note. The standard proof combines strong induction on $n$ with Euclid's lemma ( $p \mid ab \implies p \mid a \vee p \mid b$ for prime $p$ ), used to show that a prime occurring in one multiset must also occur in the other before both are reduced by cancellation.

Preamble

import Mathlib

Formal statement

namespace FundamentalTheoremOfArithmetic
theorem fta_uniqueness (n : ℕ) (hn : n ≠ 0) (l₁ l₂ : Multiset ℕ)
    (h1 : ∀ p ∈ l₁, p.Prime) (h2 : l₁.prod = n)
    (h3 : ∀ p ∈ l₂, p.Prime) (h4 : l₂.prod = n) :
    l₁ = l₂ := by sorry
end FundamentalTheoremOfArithmetic

Source

T. M. Apostol, Introduction to Analytic Number Theory, Springer, 1976, Theorem 1.10

Read-back

What the Lean code literally says, in plain math · claude-sonnet-5

This theorem, fta_uniqueness, is stated inside the namespace FundamentalTheoremOfArithmetic, under import Mathlib.

Statement. For every natural number $n : \mathbb{N}$ , every hypothesis $hn : n \neq 0$ , and every pair of multisets $l_1, l_2 : \text{Multiset}\ \mathbb{N}$ (finite unordered lists of natural numbers with multiplicity, drawn from $\mathbb{N}$ ), if

h_1 : \forall p \in l_1,\ p \text{ is prime (in the sense of } \texttt{Nat.Prime}\text{)},

h_2 : \prod_{p \in l_1} p = n \quad \text{(the product of the elements of } l_1\text{, with multiplicity, equals } n\text{)},

h_3 : \forall p \in l_2,\ p \text{ is prime},

h_4 : \prod_{p \in l_2} p = n,

then the conclusion is

l_1 = l_2,

i.e. $l_1$ and $l_2$ are equal as multisets --- the same primes occur, with exactly the same multiplicities, in both.

Details and edge cases made explicit by the statement.

$n$ ranges over all of $\mathbb{N}$ , but the hypothesis $hn : n \neq 0$ excludes $n = 0$ from consideration; the statement asserts nothing about multisets whose product is $0$ .
$l_1$ and $l_2$ are each an arbitrary Multiset ℕ --- a multiset is unordered and can contain repeated elements, so this in particular covers the case where a prime occurs with multiplicity greater than one.
$h_1$ and $h_3$ require every element of $l_1$ (resp. $l_2$ ) to satisfy Nat.Prime, Mathlib's standard primality predicate on $\mathbb{N}$ (an element $p$ is prime iff $p \geq 2$ and its only divisors are $1$ and $p$ ); nothing is asserted about elements outside the multiset, and there is no bound on the size (cardinality) of $l_1$ or $l_2$ .
Multiset.prod is taken with respect to the commutative monoid $(\mathbb{N}, \times, 1)$ ; by the stated convention, if $l_1$ (or $l_2$ ) is the empty multiset, its product is defined to be $1$ . Since $hn$ forces $n \neq 0$ , and the empty multiset's product is $1 \neq 0$ , an empty multiset is only consistent with $h_2$ (or $h_4$ ) when $n = 1$ ; for any $n \geq 2$ satisfying the hypotheses, $l_1$ and $l_2$ must be nonempty. No hypothesis explicitly forbids $l_1$ or $l_2$ from being empty in general --- this is only excluded indirectly via $n \neq 0$ together with $h_2, h_4$ when $n \neq 1$ .
The conclusion $l_1 = l_2$ is multiset equality: it asserts equality of multiplicities for every natural number, not merely that the two multisets have the same underlying set of primes, and not merely that they have the same product or the same length.
The proof of the theorem is replaced by sorry, meaning the statement is asserted but not actually proved in this code.

Human review

Endorsed by Shuze Chen · Sep 7, 2026
Endorsed by Mayank Kumar · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph