Commit 2026-02-09 22:34 17c5e1cf

View on Github →

feat: definition of a semisimple representation (#34584) Defines semisimple monoid representation and registers basic instances. Fixes a universe issue in Maschke.lean.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RepresentationTheory/FinGroupCharZero.lean

modified theorem FDRep.simple_iff_char_is_norm_one

modified theorem FDRep.simple_iff_end_is_rank_one

Modified Mathlib/RepresentationTheory/Irreducible.lean

added theorem Representation.isSimpleModule_iff_irreducible_ofModule

deleted theorem Representation.is_simple_module_iff_irreducible_ofModule

Modified Mathlib/RepresentationTheory/Maschke.lean

modified theorem LinearMap.equivariantProjection_condition

Created Mathlib/RepresentationTheory/Semisimple.lean

added theorem Representation.isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule

added theorem Representation.isSemisimpleRepresentation_iff_isSemisimpleModule_asModule