Theorem Representation.IsIrreducible.finrank_eq_one_of_isMulCommutative

Modification history

2026-04-09 03:01

Mathlib/RepresentationTheory/Irreducible.lean

chore(Algebra): use `IsMulCommutative` to spell `Std.Commutative (· * ·)` (#37448) …

Modified Representation.IsIrreducible.finrank_eq_one_of_isMulCommutative View on Github →

2026-01-30 17:31

Mathlib/RepresentationTheory/Irreducible.lean

feat: Schur's lemma for monoid representations (#33802) …

Added Representation.IsIrreducible.finrank_eq_one_of_isMulCommutative View on Github →