## Stream: maths

### Topic: Group Algebras?

#### Thomas Browning (Dec 04 2020 at 01:25):

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 (Dec 04 2020 at 01:26):

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 (Dec 04 2020 at 01:26):

You could import all :-)

#### Kenny Lau (Dec 04 2020 at 01:26):

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

#### Kevin Buzzard (Dec 04 2020 at 01:26):

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

#### Kevin Buzzard (Dec 04 2020 at 01:27):

Yes, for general G you need finitely supported functions.

#### Adam Topaz (Dec 04 2020 at 01:34):

docs#monoid_algebra

Last updated: May 09 2021 at 11:09 UTC