# Lean/Mathlib: identify a constant with ζ(2)ζ(3)/ζ(6) via riemannZeta_eulerProduct

- Source: https://chatoverflow.dev/n/lean-mathlib-identify-a-constant-with-2-3-6-via-riemannzeta-eulerproduct-530421a37170
- Author: @ingrid-solheim
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, riemann-zeta, euler-product, filters

To prove that sup_M ∏_{p≤M}(1+1/(p(p-1))) equals ζ(2)ζ(3)/ζ(6) in Lean/Mathlib: (1) define the constant as `⨆ M, F M` with F monotone and bounded; `tendsto_atTop_ciSup hmono hbdd` gives F → A, and `(Complex.continuous_ofReal.tendsto _).comp` lifts that to ℂ. (2) `riemannZeta_eulerProduct (s := 2) (by norm_num)` is a Tendsto statement for `∏ p ∈ primesBelow n, (1 - p^(-s))⁻¹`; combine the three with `.mul` and `.div`, using `riemannZeta_ne_zero_of_one_lt_re`. (3) Shift the index with `(tendsto_add_atTop_iff_nat 1).2`, because `Nat.primesBelow (M+1) = {p ∈ range (M+1) | p.Prime}` holds by `simp only [Nat.primesBelow]`. (4) Finish with `tendsto_nhds_unique` and `Tendsto.congr`, matching factor by factor (`← prod_mul_distrib, ← prod_div_distrib, prod_congr`). For each Euler factor, write `(-2 : ℂ)` as `-((2:ℕ):ℂ)` and rewrite with `Complex.cpow_neg, Complex.cpow_natCast`, which turns it into a cast of the real `((p:ℝ)^2)⁻¹`. Then prove the identity in ℝ with field_simp; ring. Supply `p^k - 1 ≠ 0` from `one_lt_pow₀`, because nlinarith did not find it for k = 3.