Mathlib Changelog
Changelog
About
Github
Commit
2022-07-24 23:44
5ed2c728
View on Github →
feat(representation_theory/Rep): Rep k G ≌ Module (monoid_algebra k G) (
#13713
)
Estimated changes
Modified
src/algebra/algebra/restrict_scalars.lean
modified
def
restrict_scalars.add_equiv
modified
theorem
restrict_scalars.add_equiv_map_smul
added
theorem
restrict_scalars.add_equiv_symm_map_algebra_map_smul
added
theorem
restrict_scalars.add_equiv_symm_map_smul_smul
added
theorem
restrict_scalars.lsmul_apply_apply
Modified
src/algebra/module/linear_map.lean
Modified
src/representation_theory/Rep.lean
added
theorem
Rep.coe_of
added
def
Rep.counit_iso
added
def
Rep.counit_iso_add_equiv
added
def
Rep.equivalence_Module_monoid_algebra
added
def
Rep.of_Module_monoid_algebra
added
theorem
Rep.of_Module_monoid_algebra_obj_coe
added
theorem
Rep.of_Module_monoid_algebra_obj_ρ
added
theorem
Rep.of_ρ
added
def
Rep.to_Module_monoid_algebra
added
def
Rep.to_Module_monoid_algebra_map
added
theorem
Rep.to_Module_monoid_algebra_map_aux
added
def
Rep.unit_iso
added
def
Rep.unit_iso_add_equiv
added
theorem
Rep.unit_iso_comm
added
def
Rep.ρ
Modified
src/representation_theory/basic.lean
modified
theorem
representation.as_algebra_hom_def
modified
theorem
representation.as_algebra_hom_of
modified
theorem
representation.as_algebra_hom_single
added
theorem
representation.as_algebra_hom_single_one
added
def
representation.as_module
added
def
representation.as_module_equiv
added
theorem
representation.as_module_equiv_map_smul
added
theorem
representation.as_module_equiv_symm_map_rho
added
theorem
representation.as_module_equiv_symm_map_smul
added
def
representation.of_module'
added
def
representation.of_module
added
theorem
representation.of_module_as_algebra_hom_apply_apply
added
theorem
representation.of_module_as_module_act
added
theorem
representation.smul_of_module_as_module
Modified
src/representation_theory/invariants.lean