Orthogonality of Dirichlet characters

Stream: PrimeNumberTheorem+

[Michael Stoll]

I think it makes sense to get the orthogonality relation for Dirichlet characters (needed for Dirichlet's Theorem) into Mathlib right away. The first PR in this context is #18659. Reviews are welcome!

See the message here for more details.