Theorem DirichletCharacter.isMultiplicative_toArithmeticFunction

Modification history

2024-11-01 12:21
Mathlib/NumberTheory/LSeries/Dirichlet.lean
feat(NumberTheory/LSeries/QuadraticNonvanishing): new file (#18302) …
Added DirichletCharacter.isMultiplicative_toArithmeticFunctionView on Github →