Theorem Rep.trivial_def

Modification history

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 →