feat: modular characters

[erdOne]

Co-authored-by: Yaël Dillies
Co-authored-by: Javier López-Contreras

[Ruben-VandeVelde]

Please add the copyright header

[YaelDillies]

We forgot the most important statement! μ (g • s) = modularHaarChar A g • μ s

Also, you should update the Co-authored-by

[erdOne]

We forgot the most important statement! μ (g • s) = modularHaarChar A g • μ s

Not entirely sure what's the right typeclass to add to get this. I've added [IsFiniteMeasureOnCompacts μ] [Regular μ] for now and I hope we have this in our application.

[kbuzzard]

I bumped mathlib and broke this PR. Sorry! Error is

'MeasureTheory.Measure.addHaarScalarFactor_eq_mul' has already been declared

in FLT.Mathlib.MeasureTheory.Measure.Haar.Unique .

[YaelDillies]

I believe that's just Andrew having been super efficient with upstreaming 😁 You can simply delete the FLT.Mathlib.MeasureTheory.Measure.Haar.Unique file and replace it by Mathlib.MeasureTheory.Measure.Haar.Unique where it is imported

[pitmonticone]

Done.

[YaelDillies]

Can you run lake exe mk_all?

[pitmonticone]

Done.

[kbuzzard]

Thanks!