mathlib
b9430470 - feat(representation_theory/fdRep): Schur's lemma (#13794)

Commit
3 years ago
feat(representation_theory/fdRep): Schur's lemma (#13794) In fact, we've had Schur's lemma in mathlib for over a year, since #7366, but this was stated very abstractly: for any linear category over an algebraically closed field with finite dimensional hom spaces, and kernels. Finally, `fdRep k G` satisfies all those hypotheses, so we can use Schur's lemma! Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading