Multiplicative characters of finite groups

Stream: Is there code for X?

[Daniel Weber]

Are basic lemmas on multiplicative characters of finite groups proven in mathlib? In particular, I'm interested in orthogonality.

[Daniel Weber]

Oh, I found Mathlib.NumberTheory.LegendreSymbol.MulCharacter. Should've looked in number theory

[Notification Bot]

Command Master has marked this topic as resolved.

[Notification Bot]

Command Master has marked this topic as unresolved.

[Daniel Weber]

Actually, my domain isn't a ring, only a group. Is there something for this case?

[Daniel Weber]

Oh, actually I see that the definition is for a monoid, but the theorem I need, MulChar.IsNontrivial.sum_eq_zero, requires that the domain is a ring.

[Kevin Buzzard]

docs#MulChar.IsNontrivial.sum_eq_zero

[Michael Stoll]

OK; I'll see to what extent the CommRing assumption can be weakened to CommMonoidhere.

[Daniel Weber]

Yes, I found this, but this requires the domain to be a ring and mine is only a group.

[Kevin Buzzard]

I know you found it, I was just looking to see what it said :-) (if you write it like that on Zulip it makes a link)

[Michael Stoll]

(I just checked that the proof still works. But I have to go through the file more systematically...)

[Michael Stoll]

#11012
Should be easy to review...

[Daniel Weber]

I see it was merged, thanks! A bit unrelated, but how do I update mathlib? When I run lake update I get error: project: could not rename packages directory (.\.lake/packages -> .\.lake\packages): no error (error code: 0)

[Daniel Weber]

By the way, I think this can also be done for (at least some of) docs#AddChar

[Ruben Van de Velde]

That's a new error for me. Just to be clear: are you updating your independent copy of the mathlib repository, or mathlib as a dependency of another project?

[Damiano Testa]

Indeed, and the mismatch / is \ is weird.

[Daniel Weber]

Ruben Van de Velde said:

That's a new error for me. Just to be clear: are you updating your independent copy of the mathlib repository, or mathlib as a dependency of another project?

As a dependency.

[Ruben Van de Velde]

I would try to remove the .lake folder manually and then run lake update again

[Daniel Weber]

That works, thanks

[Michael Stoll]

Command Master said:

By the way, I think this can also be done for (at least some of) docs#AddChar

#11049 for similar improvements to additive characters.

[Richard Copley]

Command Master said:

I see it was merged, thanks! A bit unrelated, but how do I update mathlib? When I run lake update I get error: project: could not rename packages directory (.\.lake/packages -> .\.lake\packages): no error (error code: 0)

I suspect you just needed to shut down instances of lake and lean running in your project directory, for example by closing your editor.