Commit 2025-11-04 15:34 dd476c78

feat(RepresentationTheory/FinGroupCharZero): applications of Maschke's theorem (#27429) Prove some properties of representations that follow from Maschke's theorem:

• If G is a finite group whose order is invertible in a field k, then every object of Rep k G (resp. FDRep k G) is injective and projective.
• For an object V of FDRep k G, when k is an algebraically closed field in which the order of G is invertible: (1) V is simple if and only V ⟶ V is a k-vector space of dimension 1 (FDRep.simple_iff_end_is_rank_one); (2) When k is characteristic zero, V is simple if and only if ∑ g : G, V.character g * V.character g⁻¹ = Fintype.card G (FDRep.simple_iff_char_is_norm_one). Note: This used to be #27165, but it was closed for some reason I don't understand.

• depends on: #27154
• depends on: #27134
• depends on: #27125