Commit 2024-02-01 14:46 618b0bbd

View on Github →

feat(RepresentationTheory/Action): add ofMulAction constructor for FintypeCat (#9665) Adds the analogue of Action.ofMulAction for FintypeCat.

Estimated changes

Modified Mathlib/RepresentationTheory/Action/Concrete.lean

added def Action.FintypeCat.ofMulAction

added theorem Action.FintypeCat.ofMulAction_apply