Theorem DirichletCharacter.LFunction_at_one_ne_zero_of_quadratic

Modification history

2024-11-18 10:53

Mathlib/NumberTheory/LSeries/QuadraticNonvanishing.lean

refactor(NumberTheory/LSeries): merge `QuadraticNonvanishing` into `Nonvanishing` (#19185) …

Deleted DirichletCharacter.LFunction_at_one_ne_zero_of_quadratic View on Github →

2024-11-01 12:21

Mathlib/NumberTheory/LSeries/QuadraticNonvanishing.lean

feat(NumberTheory/LSeries/QuadraticNonvanishing): new file (#18302) …

Added DirichletCharacter.LFunction_at_one_ne_zero_of_quadratic View on Github →