Commit 2024-11-01 12:21 28b73442

feat(NumberTheory/LSeries/QuadraticNonvanishing): new file (#18302) We add a new file whose main result is

theorem LFunction_at_one_ne_zero_of_quadratic {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N}
    (hχ : χ ^ 2 = 1) (χ_ne : χ ≠ 1) :
    χ.LFunction 1 ≠ 0 := by

which is needed to prove Dirichlet's Theorem on primes in AP.