Def Action.forget

Modification history

2023-12-05 09:47

Mathlib/RepresentationTheory/Action.lean

chore: split RepresentationTheory.Action in multiple files (#8660) …

Modified Action.forget View on Github →

2023-06-06 18:52

Mathlib/RepresentationTheory/Action.lean

feat: port RepresentationTheory.Action (#4700)

Added Action.forget View on Github →