Theorem Representation.smul_ofModule_asModule

Modification history

2025-12-08 07:46
Mathlib/RepresentationTheory/Basic.lean
feat(Algebra/MonoidAlgebra): extend the `R[M]` notation to `MonoidAlgebra R M` (#30877) …
Modified Representation.smul_ofModule_asModuleView on Github →
2023-05-23 17:21
Mathlib/RepresentationTheory/Basic.lean
feat: port RepresentationTheory.Basic (#4240)
Added Representation.smul_ofModule_asModuleView on Github →