Theorem DirichletCharacter.norm_le_one

Modification history

2023-11-27 20:16
Mathlib/NumberTheory/DirichletCharacter/Bounds.lean
feat: bounds for Dirichlet characters (#8449) …
Added DirichletCharacter.norm_le_oneView on Github →