Theorem Representation.ofMulAction_self_smul_eq_mul

Modification history

2026-07-04 08:56
Mathlib/RepresentationTheory/Basic.lean
refactor(Algebra): make `MonoidAlgebra` into a one-field structure (#38714) …
Deleted Representation.ofMulAction_self_smul_eq_mulView on Github →
2025-12-08 07:46
Mathlib/RepresentationTheory/Basic.lean
feat(Algebra/MonoidAlgebra): extend the `R[M]` notation to `MonoidAlgebra R M` (#30877) …
Modified Representation.ofMulAction_self_smul_eq_mulView on Github →
2023-05-23 17:21
Mathlib/RepresentationTheory/Basic.lean
feat: port RepresentationTheory.Basic (#4240)
Added Representation.ofMulAction_self_smul_eq_mulView on Github →