Def FdRep.character

Modification history

2024-07-11 19:31

Mathlib/RepresentationTheory/Character.lean

chore(RepresentationTheory): rename FdRep to FDRep (#14309) …

Deleted FdRep.character View on Github →

2023-07-03 11:03

Mathlib/RepresentationTheory/Character.lean

feat: port RepresentationTheory.Character (#5679)

Added FdRep.character View on Github →