Commit 2023-11-27 20:16 c77ae20f
View on Github →feat: bounds for Dirichlet characters (#8449)
This adds NumberTheory.DirichletCharacter.Bounds containing proofs of ‖χ a‖ = 1 if a is a unit and ‖χ a‖ ≤ 1 in general, where χ is a Dirichlet character with values in a normed field.
There are also two API lemmas added elsewhere that are used in the proofs.