Theorem DirichletCharacter.conductor_eq_zero_iff_level_eq_zero

Modification history

2023-10-23 09:15
Mathlib/NumberTheory/DirichletCharacter/Basic.lean
feat: properties of the conductor (#7352)
Added DirichletCharacter.conductor_eq_zero_iff_level_eq_zeroView on Github →