Theorem Representation.irreducible_iff_isSimpleModule_asModule

Modification history

2026-01-23 08:59
Mathlib/RepresentationTheory/Irreducible.lean
feat: definition of an irreducible representation (#32856) …
Added Representation.irreducible_iff_isSimpleModule_asModuleView on Github →