From 1b424cf74f136ad55e9fe04fafda0f63c710a342 Mon Sep 17 00:00:00 2001 From: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> Date: Mon, 28 Oct 2024 10:25:16 +0100 Subject: [PATCH] Apply docstring fixes from code review Co-authored-by: Jz Pan --- Mathlib/NumberTheory/LSeries/QuadraticNonvanishing.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/LSeries/QuadraticNonvanishing.lean b/Mathlib/NumberTheory/LSeries/QuadraticNonvanishing.lean index ce844268226cf..00b684a118407 100644 --- a/Mathlib/NumberTheory/LSeries/QuadraticNonvanishing.lean +++ b/Mathlib/NumberTheory/LSeries/QuadraticNonvanishing.lean @@ -83,13 +83,13 @@ lemma zetaMul_nonneg {χ : DirichletCharacter ℂ N} (hχ : χ ^ 2 = 1) (n : ℕ /-! ### "Bad" Dirichlet characters -Our goal is to show that `L χ 1 ≠ 0` when `χ` is a (nontrivial) quadratic Dirichlet character. +Our goal is to show that `L(χ, 1) ≠ 0` when `χ` is a (nontrivial) quadratic Dirichlet character. To do that, we package the contradictory properties in a structure `DirichletCharacter.BadChar` and derive further statements eventually leading to a contradiction. -/ /-- The object we're trying to show doesn't exist: A nontrivial quadratic Dirichlet character -whose L-function vanishes at `s =1`. -/ +whose L-function vanishes at `s = 1`. -/ structure BadChar (N : ℕ) [NeZero N] where /-- The character we want to show cannot exist. -/ χ : DirichletCharacter ℂ N