Dirichlet characters

Stream: PR reviews

[Moritz Firsching]

@Ashvni Narayanan and I plan to port the main parts of https://github.com/laughinggas/p-adic-L-functions to lean 4 and adding them to mathlib, starting with the basics of Dirichlet characters.
#7010 the draft pull request for the first part of that: while it is not quite ready for review yet, comments would be welcome!

[Moritz Firsching]

The very first pull request for Dirichlet characters is now ready for review: #7010. Feedback is especially welcome since this is the definition much of the further stuff builds on...

[Michael Stoll]

I'd like to add

lemma DirichletCharacter.norm_le_one {n : ℕ} (χ : DirichletCharacter ℂ n) (m : ZMod n) :
    ‖χ m‖ ≤ 1 := ...

to NumberTheory.DirichletCharacter.Basic.
@Ashvni Narayanan @Moritz Firsching Is this OK for you, or should this go into a separate file? What are your plans for further files below NumberTheory.DirichletCharacter?

[Joachim Breitner]

Im surprised that we need Dirichlet characters - are Unicode characters not sufficient after all?

[Moritz Firsching]

That sounds great, @Michael Stoll! I think it is fine to go in the same file. @Ashvni Narayanan knows the plans for file further down.

[Michael Stoll]

I have suggested in a PM to Avshni (no reply yet) to put this into a separate file, as it needs some more imports. I have proposed to use "Properties.lean" since this is the name used in the lean3 repo, but maybe a more descriptive name like "Bounds.lean" would make sense. What do you think?

[Moritz Firsching]

Bounds.lean or perhaps Norm.lean sounds good to me. I guess it would be a nice not to have too many imports and keep the files small.

I just made a pr proposing to add reduction of a DirichletCharacter to Basic.lean, following @Ashvni Narayanan . Other than that the plan is mainly to add a few things for even and odd.

[Michael Stoll]

The bounds are in #8449.

[Ashvni Narayanan]

Hi @Michael Stoll , I did reply to your PM a few days ago, I am now unsure if you received it. Apologies if my message was unclear, I meant to say that Properties.lean would be fine. Bounds.lean is also ok, it will probably be a relatively small file, which may be better, I am unsure.

[Michael Stoll]

@Ashvni Narayanan Your message was not unclear, but I thought that a separate file for the bounds makes sense.
I'll have another look at your PR tomorrow (was traveling today).