Group Algebras?

Stream: maths

[Thomas Browning]

Does mathlib have group algebras yet (i.e., FG where F is a field and G is a finite group)? I can't find it mentioned in the usual places, but it seems like a sort of thing where a disguised version (i.e., a ring structure on functions from G to F) might be hidden somewhere.

[Kevin Buzzard]

If G is finite it's just F -> G G -> F, so you could check to see if there's a ring structure on that if G is a fintype and a group, and F is a field (or a commutative ring).

[Kevin Buzzard]

You could import all :-)

[Kenny Lau]

it's G \to\0 F (fin. supp. functions) right

[Kevin Buzzard]

Oh I went the wrong way :D (I think it's time for bed)

[Kevin Buzzard]

Yes, for general G you need finitely supported functions.

[Adam Topaz]

docs#monoid_algebra