LSeries_one_mul_Lseries_moebius — Mathlib

English

For Re(s) > 1, the L-series of ζ and the L-series of μ are inverses: L((↗ζ), s) · L((↗μ), s) = 1.

Русский

Для Re(s) > 1 произведение L-серий дзеты и Моебиуса равно единице: L((↗ζ), s) · L((↗μ), s) = 1.

LaTeX

$$$1 < \\operatorname{Re}(s) \\Rightarrow L(↗ζ,s) \\cdot L(↗μ,s) = 1$$$

Lean4

/-- The L-series of the constant sequence `1` and of the Möbius function are inverses. -/
theorem LSeries_one_mul_Lseries_moebius {s : ℂ} (hs : 1 < s.re) : L 1 s * L (↗μ) s = 1 :=
  LSeries_zeta_eq ▸ LSeries_zeta_mul_Lseries_moebius hs

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