LFunctionTrivChar₁ — Mathlib

English

For all n, LFunctionTrivChar₁ n 1 ≠ 0.

Русский

Для любого n, LFunctionTrivChar₁ n в s=1 не равно нулю.

LaTeX

$$$LFunctionTrivChar_1(n,1) \neq 0$$$

Lean4

/-- The function obtained by "multiplying away" the pole of `L χ` for a trivial Dirichlet
character `χ`. Its (negative) logarithmic derivative is used to prove Dirichlet's Theorem
on primes in arithmetic progression. -/
noncomputable abbrev LFunctionTrivChar₁ : ℂ → ℂ :=
  Function.update (fun s ↦ (s - 1) * LFunctionTrivChar n s) 1 (∏ p ∈ n.primeFactors, (1 - (p : ℂ)⁻¹))

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