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

AUTHOR

Daniel de Rauglaudre

ROCQ VERSION

The Rocq Prover, version 9.0.0
compiled with OCaml 4.14.1