Commit 2023-05-23 17:21 7c0f06ff

View on Github →

feat: port RepresentationTheory.Basic (#4240)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RepresentationTheory/Basic.lean

added theorem Representation.asAlgebraHom_def

added theorem Representation.asAlgebraHom_of

added theorem Representation.asAlgebraHom_single

added theorem Representation.asAlgebraHom_single_one

added def Representation.asGroupHom

added theorem Representation.asGroupHom_apply

added def Representation.asModule

added def Representation.asModuleEquiv

added theorem Representation.asModuleEquiv_map_smul

added theorem Representation.asModuleEquiv_symm_map_rho

added theorem Representation.asModuleEquiv_symm_map_smul

added def Representation.dual

added theorem Representation.dualTensorHom_comm

added theorem Representation.dual_apply

added def Representation.linHom

added theorem Representation.linHom_apply

added theorem Representation.ofModule_asAlgebraHom_apply_apply

added theorem Representation.ofModule_asModule_act

added theorem Representation.ofMulAction_apply

added theorem Representation.ofMulAction_def

added theorem Representation.ofMulAction_self_smul_eq_mul

added theorem Representation.ofMulAction_single

added theorem Representation.smul_ofModule_asModule

added theorem Representation.smul_one_tprod_asModule

added theorem Representation.smul_tprod_one_asModule

added def Representation.tprod

added theorem Representation.tprod_apply

added def Representation.trivial

added theorem Representation.trivial_def