Theorem Representation.free_asModule_free

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.free_asModule_freeView on Github →
2025-05-30 11:19
Mathlib/RepresentationTheory/Basic.lean
feat(RepresentationTheory/*): representations on `Finsupp` (#21732) …
Added Representation.free_asModule_freeView on Github →