# Zulip Chat Archive

## Stream: maths

### Topic: group representations

#### Greg Conneen (Nov 14 2019 at 23:52):

Is there any representation theory in Mathlib? I can't seem to find any. If there isn't, how would I go about defining a representation, characters, and stating/proving things like Schur's Lemma? I've been fuddling around and need a little guidance.

#### Alex J. Best (Nov 14 2019 at 23:59):

I think someone asked the same question a month back, you should be able to find the thread by searching zulip for representation theory

#### Greg Conneen (Nov 15 2019 at 00:10):

When I searched for this topic beforehand, this is all I found:

class representation (G R M : Type) [monoid G] [ring R] [add_comm_group M] [module R M] extends group_module G M := (smul_comm : ∀ (g : G) (r : R) (m : M), g • (r • m) = r • (g • m)) namespace representation open mul_action linear_map variables {G R M : Type} variables [group G] [ring R] [add_comm_group M] [module R M] [representation G R M] -- set_option trace.class_instances true -- lemma smul_mem_fixed_points (r : R) (m : M) (hm : m ∈ fixed_points G M) : -- r • m ∈ fixed_points G M := -- begin -- simp only [mem_fixed_points] at *, -- intro g, -- rw [smul_comm, hm], -- end end representation

I read through that thread, and didn't exactly see a lot of development, just attempts at explaining the code, so it's not exactly what I'm looking for.

#### Alex J. Best (Nov 15 2019 at 01:41):

Right, I think the result of that thread is that no, there isn't any! But lots of people would be interested in seeing some.

Last updated: May 14 2021 at 19:21 UTC