Theorem DirichletCharacter.unit_norm_eq_one

Modification history

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