Def Action.FintypeCat.ofMulAction

Modification history

2025-05-02 13:41
Mathlib/CategoryTheory/Action/Concrete.lean
chore(CategoryTheory/Action): generalize universes (#24547) …
Modified Action.FintypeCat.ofMulActionView on Github →
2024-02-01 14:46
Mathlib/RepresentationTheory/Action/Concrete.lean
feat(RepresentationTheory/Action): add `ofMulAction` constructor for `FintypeCat` (#9665) …
Added Action.FintypeCat.ofMulActionView on Github →