Skip to content

Commit

Permalink
Apply docstring fixes from code review
Browse files Browse the repository at this point in the history
Co-authored-by: Jz Pan <[email protected]>
  • Loading branch information
MichaelStollBayreuth and acmepjz authored Oct 28, 2024
1 parent 17eb2fd commit 1b424cf
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Mathlib/NumberTheory/LSeries/QuadraticNonvanishing.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 1b424cf

Please sign in to comment.