Def Rep.mkQ

Modification history

2026-03-24 21:13

Mathlib/RepresentationTheory/Rep.lean

chore(RepresentationTheory): Refactor Rep (#36127) …

Modified Rep.mkQ View on Github →

2025-05-15 10:23

Mathlib/RepresentationTheory/Rep.lean

feat(RepresentationTheory/*): subrepresentations, quotients by subrepresentations, and representations of quotient groups (#22651) …

Added Rep.mkQ View on Github →