Theorem FDRep.simple_iff_char_is_norm_one

Modification history

2025-11-04 15:34
Mathlib/RepresentationTheory/FinGroupCharZero.lean
feat(RepresentationTheory/FinGroupCharZero): applications of Maschke's theorem (#27429) …
Added FDRep.simple_iff_char_is_norm_oneView on Github →