Theorem Rep.trivial_def

Modification history

2026-03-24 21:13

Mathlib/RepresentationTheory/Rep.lean

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

Deleted Rep.trivial_def View on Github →

2025-02-27 23:06

Mathlib/RepresentationTheory/Rep.lean

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

Modified Rep.trivial_def View on Github →

2023-06-21 09:25

Mathlib/RepresentationTheory/Rep.lean

feat: port RepresentationTheory.Rep (#5041)

Added Rep.trivial_def View on Github →