appease linter

leanprover-community · Oct 27, 2024 · 17eb2fd · 17eb2fd
1 parent 2cdf288
commit 17eb2fd
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/NumberTheory/LSeries/QuadraticNonvanishing.lean b/Mathlib/NumberTheory/LSeries/QuadraticNonvanishing.lean
@@ -91,6 +91,7 @@ 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`. -/
 structure BadChar (N : ℕ) [NeZero N] where
+  /-- The character we want to show cannot exist. -/
   χ : DirichletCharacter ℂ N
   χ_ne : χ ≠ 1
   χ_sq : χ ^ 2 = 1