monoid_algebra.char_p

Stream: general

[Johan Commelin]

If k has characteristic p, then so does monoid_algebra k G. Where in the library do we put those facts? I don't think that data.monoid_algebra should import char_p stuff. But vice versa also doesn't make sense. Do we start a new file for such things?

[Kevin Buzzard]

rep theory in char p has a completely different flavour to char 0 so there's an argument for making a new file

[Johan Commelin]

Well, this lemma would also be used to show that mv_polynomial \s rat has characteristic 0. I wouldn't want to import rep'n theory in char p for that...

[Johan Commelin]

So it's lower level than that.

[Scott Morrison]

Why don't we just do this after the mv_polynomial file?

[Scott Morrison]

There's no rule that says everything about multivariable polynomials has to be in that file.

[Scott Morrison]

(Indeed, I'd say the opposite: only the minimal possible should be in that file.)

[Scott Morrison]

How about just put facts like this in representation_theory/char_p/basic.lean?

[Johan Commelin]

Maybe that's a nice place to put it