Documentation
LeanPool
.
LeanModularForms
.
Modularforms
.
RiemannZetalems
Search
return to top
source
Imports
Init
Mathlib.Analysis.CStarAlgebra.Classes
Mathlib.NumberTheory.LSeries.RiemannZeta
Mathlib.Algebra.Order.Star.Real
Imported by
zeta_two_eqn
RiemannZetalems
#
source
theorem
zeta_two_eqn
:
∑'
(
n
:
ℤ
)
,
(
↑
n
^
2
)
⁻¹
=
2
*
riemannZeta
2