Def Rep.trivial

Modification history

2025-02-27 23:06

Mathlib/RepresentationTheory/Rep.lean

refactor(RepresentationTheory/*): minor tweaks to the API for trivial representations (#22335)

Deleted Rep.trivial View on Github →

2023-06-21 09:25

Mathlib/RepresentationTheory/Rep.lean

feat: port RepresentationTheory.Rep (#5041)

Added Rep.trivial View on Github →