Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-27 02:01 cb2b02ff

View on Github →

feat(representation_theory/basic): representation theory without scalar actions (#13573) This PR rewrites the files representation_theory/basic and representation_theory/invariants so that they avoid making use of scalar actions. It also includes the new definitions and lemmas of PR #13502 written with this new approach.

Estimated changes

Modified src/representation_theory/basic.lean

added theorem representation.as_algebra_hom_of

added theorem representation.as_group_hom_apply

deleted theorem representation.as_module_apply

modified theorem representation.char_conj

added theorem representation.char_mul_comm

modified theorem representation.char_one

added def representation.dual

added theorem representation.dual_apply

added def representation.lin_hom

added theorem representation.lin_hom_apply

deleted theorem representation.of_smul

added def representation.tprod

added theorem representation.tprod_apply

added def representation.trivial

added theorem representation.trivial_def

added def representation

Modified src/representation_theory/invariants.lean

added theorem group_algebra.average_def

added theorem group_algebra.mul_average_left

added theorem group_algebra.mul_average_right

deleted theorem representation.average_def

added theorem representation.average_map_id

added theorem representation.average_map_invariant

deleted theorem representation.invariants'_carrier

modified theorem representation.mem_invariants

deleted theorem representation.mul_average_left

deleted theorem representation.mul_average_right

deleted theorem representation.smul_average_id

deleted theorem representation.smul_average_invariant