Theorem Action.FintypeCat.ofMulAction_apply

Modification history

2025-05-02 13:41

Mathlib/CategoryTheory/Action/Concrete.lean

chore(CategoryTheory/Action): generalize universes (#24547) …

Modified Action.FintypeCat.ofMulAction_apply View on Github →

2024-02-01 14:46

Mathlib/RepresentationTheory/Action/Concrete.lean

feat(RepresentationTheory/Action): add `ofMulAction` constructor for `FintypeCat` (#9665) …

Added Action.FintypeCat.ofMulAction_apply View on Github →