Euler's totient function #
This file defines Euler's totient function
Nat.totient n
which counts the number of naturals less than n
that are coprime with n
.
We prove the divisor sum formula, namely that n
equals φ
summed over the divisors of n
. See
sum_totient
. We also prove two lemmas to help compute totients, namely totient_mul
and
totient_prime_pow
.
Euler's totient function. This counts the number of naturals strictly less than n
which are
coprime with n
.
Equations
Instances For
Euler's totient function. This counts the number of naturals strictly less than n
which are
coprime with n
.
Equations
Instances For
Euler's product formula for the totient function #
We prove several different statements of this formula.
Euler's product formula for the totient function.
Euler's product formula for the totient function.
Euler's product formula for the totient function.