Theorem Representation.trivial_def

Modification history

2025-02-27 23:06

Mathlib/RepresentationTheory/Basic.lean

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

Deleted Representation.trivial_def View on Github →

2023-05-23 17:21

Mathlib/RepresentationTheory/Basic.lean

feat: port RepresentationTheory.Basic (#4240)

Added Representation.trivial_def View on Github →