Commit 2022-04-10 01:48 d1338749

View on Github →

feat(representation_theory/basic): basics of group representation theory (#11207) Some basic lemmas about group representations and some theory regarding the subspace of fixed points of a representation.

Estimated changes

Modified src/algebra/monoid_algebra/basic.lean

added theorem monoid_algebra.smul_of

added def monoid_algebra.submodule_of_smul_mem

Created src/representation_theory/basic.lean

added theorem representation.as_algebra_hom_def

added theorem representation.as_algebra_hom_single

added def representation.as_group_hom

added theorem representation.as_module_apply

added theorem representation.char_conj

added theorem representation.char_one

added theorem representation.of_smul

Created src/representation_theory/invariants.lean

added theorem representation.average_def

added theorem representation.invariants'_carrier

added def representation.invariants

added theorem representation.invariants_eq_inter

added theorem representation.mem_invariants

added theorem representation.mul_average_left

added theorem representation.mul_average_right

added theorem representation.smul_average_id

added theorem representation.smul_average_invariant