Documentation
SpherePacking
.
ModularForms
.
riemannZetalems
Search
return to top
source
Imports
Init
Mathlib.Analysis.CStarAlgebra.Classes
Mathlib.Data.Real.StarOrdered
Mathlib.NumberTheory.LSeries.RiemannZeta
Imported by
zeta_two_eqn
source
theorem
zeta_two_eqn
:
∑'
(
n
:
ℤ
)
,
(
↑
n
^
2
)
⁻¹
=
2
*
riemannZeta
2