ζ(5) as a real number

noncomputable def Zeta5Irrational.zeta5 : ℝ

ζ(5) as a real number.

Equations

• Zeta5Irrational.zeta5 = ∑' (n : ℕ), 1 / ↑n ^ 5

theorem Zeta5Irrational.riemannZeta_five : riemannZeta 5 = ↑zeta5

Mathlib's riemannZeta 5 is the real number zeta5.