Theorems · Theorem · number theory

Nat.primeFactorsList_unique

• #80 of the 100 theorems: The Fundamental Theorem of Arithmetic
• 1000+ list: Fundamental theorem of arithmetic

∀ {n : ℕ} {l : List ℕ}, l.prod = n → (∀ p ∈ l, Nat.Prime p) → l.Perm n.primeFactorsList

Fundamental theorem of arithmetic

Defined in

Mathlib.Data.Nat.Factors

Cited by

3 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound