Theorem Representation.isTrivial_def

Modification history

2025-02-27 23:06
Mathlib/RepresentationTheory/Basic.lean
refactor(RepresentationTheory/*): minor tweaks to the API for trivial representations (#22335)
Added Representation.isTrivial_defView on Github →