Coq proof of the Euler product formula for the Riemann zeta function
Σ (n ∈ ℕ*) 1/n^s = Π (p ∈ Primes) 1/(1-1/n^p)
Work in progress...
Some other proofs in prime numbers, not necessarily connected to that proof:
- About the totient function φ
- About quadratic residues
- Lagrange's theorem of four squares
Daniel de Rauglaudre
The Coq Proof Assistant, version 8.14+alpha compiled with OCaml 4.12.0