Prime numbers #
This file deals with the factors of natural numbers.
Important declarations #
Nat.primeFactorsList n
: the prime factorization ofn
Nat.primeFactorsList_unique
: uniqueness of the prime factorisation
primeFactorsList n
is the prime factorization of n
, listed in increasing order.
Equations
- Nat.primeFactorsList 0 = []
- Nat.primeFactorsList 1 = []
- k.succ.succ.primeFactorsList = (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList
Instances For
Alias of Nat.isChain_cons_primeFactorsList
.
Alias of Nat.isChain_two_cons_primeFactorsList
.
Alias of Nat.isChain_primeFactorsList
.
primeFactorsList
can be constructed inductively by extracting minFac
, for sufficiently
large n
.
Fundamental theorem of arithmetic
For positive a
and b
, the prime factors of a * b
are the union of those of a
and b
For coprime a
and b
, the prime factors of a * b
are the union of those of a
and b
The sets of factors of coprime a
and b
are disjoint
If p
is a prime factor of a
then p
is also a prime factor of a * b
for any b > 0
If p
is a prime factor of b
then p
is also a prime factor of a * b
for any a > 0