hasSum_zeta_two — Mathlib

English

The Basel problem value: ζ(2) = π^2/6.

Русский

Значение задачи Баттерса: ζ(2) = π^2/6.

LaTeX

$$$\displaystyle \sum_{n=1}^{\infty} \frac{1}{n^{2}} = \frac{\pi^{2}}{6}. $$$

Lean4

theorem hasSum_zeta_two : HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 2) (π ^ 2 / 6) :=
  by
  convert hasSum_zeta_nat one_ne_zero using 1; rw [mul_one]
  rw [bernoulli_eq_bernoulli'_of_ne_one (by decide : 2 ≠ 1), bernoulli'_two]
  norm_num [Nat.factorial]; field_simp

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