Def FDRep.of

Modification history

2025-02-06 10:13

Mathlib/RepresentationTheory/FDRep.lean

refactor(RepresentationTheory): `ConcreteCategory` instances for `Rep` (#21465) …

Deleted FDRep.of View on Github →

2024-07-11 19:31

Mathlib/RepresentationTheory/FDRep.lean

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

Added FDRep.of View on Github →