Def Rep.toModuleMonoidAlgebra

Modification history

2025-12-08 07:46

Mathlib/RepresentationTheory/Rep.lean

feat(Algebra/MonoidAlgebra): extend the `R[M]` notation to `MonoidAlgebra R M` (#30877) …

Modified Rep.toModuleMonoidAlgebra View on Github →

2023-06-21 09:25

Mathlib/RepresentationTheory/Rep.lean

feat: port RepresentationTheory.Rep (#5041)

Added Rep.toModuleMonoidAlgebra View on Github →