Theorem Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed

Modification history

2026-01-30 17:31
Mathlib/RepresentationTheory/Irreducible.lean
feat: Schur's lemma for monoid representations (#33802) …
Added Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosedView on Github →