Towards Cyclotomic Character

Stream: mathlib4

[Qi Ge]

Hi all, I've been working towards defining the $p$-adic cyclotomic character. This is what I got so far.
In particular I took the natural group theory approach that

1. Define the group isomorphism between the endomorphisms of a finite cyclic group with ZMod of its cardinality
2. Using its properties to define ModularCyclotomicCharacter and show for compatibilities.

My understanding is that the current API for Z[p] is still insufficient to get a map easily. So there is still work to do to get the $p$-adic cyclotomic character.
I'm thinking about refining and organizing what I have so far, and push to mathlib since it is getting harder to manage as it gets longer.

I'm aware ModularCyclotomicCharacter is already done in mathlib4#6342 by @Kevin Buzzard.
@Adam Topaz told me a sensible plan could be to show that my implementation would agree with what is in mathlib right now.
All inputs are welcomed!

[Qi Ge]

In particular:
L14-L135 are variously lemmas that definitely need be cleaned up.
L137-L437 concern endomorphisms of finite cyclic (multiplicative/additive) group.
L439-L495 get to ModularCyclotomicCharacter and their compatibility.

[Adam Topaz]

I haven't looked through everything yet, but I surely hope that your lemma Group.exponent_dvd_of_forall_pow_eq_one already exists in some form in mathlib!

[Yaël Dillies]

docs#Monoid.exponent_dvd_of_forall_pow_eq_one

[Adam Topaz]

Oh I see, that's for monoids with n : Nat, but I guess @Qi Ge needed it for groups with n : Int.

[Yaël Dillies]

Oh yeah we don't have that