Up to index of Isabelle/HOL/HOL-Complex
View theory dependencies
We inherited the following files from the Isabelle 2002 distribution:
Some basic libraries:
Unique factorization for the integers, and multiplicity:
A proof of Gauss's law of quadratic reciprocity:
More elementary number theory, including Möbius inversion:
Libraries for the reals and big O calculations, and the partial summation formula:
Identities involving ln:
Chebyshev's theorems:
The main proof of the prime number theorem: