riemannZeta_two — Mathlib

English

The Riemann zeta function at 4 equals π^4/90: ζ(4) = π^4/90.

Русский

Зета-функция Римана в точке 4 равна π^4/90: ζ(4) = π^4/90.

LaTeX

$$$$ \operatorname{riemannZeta}(4) = \frac{\pi^4}{90}. $$$$

Lean4

theorem riemannZeta_two : riemannZeta 2 = (π : ℂ) ^ 2 / 6 :=
  by
  convert congr_arg ((↑) : ℝ → ℂ) hasSum_zeta_two.tsum_eq
  · rw [← Nat.cast_two, zeta_nat_eq_tsum_of_gt_one one_lt_two]
    simp [push_cast]
  · norm_cast

Похожие утверждения