Commit 2023-07-02 17:59 9dd08868

View on Github →

feat: port RepresentationTheory.Invariants (#5655)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RepresentationTheory/Invariants.lean

added theorem GroupAlgebra.mul_average_left

added theorem GroupAlgebra.mul_average_right

added theorem Representation.averageMap_id

added theorem Representation.averageMap_invariant

added def Representation.invariants

added theorem Representation.invariants_eq_inter

added theorem Representation.isProj_averageMap

added def Representation.linHom.invariantsEquivFdRepHom

added def Representation.linHom.invariantsEquivRepHom

added theorem Representation.linHom.mem_invariants_iff_comm

added theorem Representation.mem_invariants