feat(NumberTheory/LSeries/QuadraticNonvanishing): new file

[MichaelStollBayreuth]

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.

---

[github-actions]

PR summary 1b424cf74f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.LSeries.QuadraticNonvanishing	2295

---

Declarations diff

+ BadChar
+ F
+ F_differentiable
+ F_differentiableAt_of_ne
+ F_eq_LSeries
+ F_neg_two
+ HasDerivAt.continuousAt_div
+ LFunction_at_one_ne_zero_of_quadratic
+ LSeriesSummable_zetaMul
+ apply_eq_toArithmeticFunction_apply
+ isMultiplicative_toArithmeticFunction
+ isMultiplicative_zetaMul
+ isQuadratic_iff_sq_eq_one
+ zetaMul
+ zetaMul_nonneg
+ zetaMul_prime_pow_nonneg

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[MichaelStollBayreuth]

@loefflerd @CBirkbeck I have restructured the code for the nonvanishing of the L-function of quadratic Dirichlet characters at s = 1. In particular (and as envisaged) I have split the main part of the code into properties of the convolution with zeta on the ode side (which might be useful in other contexts) and properties that need the (false) assumption that L χ 1 = 0. (Plus some golfing.) Your reviews are welcome!

[acmepjz]

Found some typo.