Commit 2025-02-27 23:06 407bc37f

View on Github →

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

Estimated changes

Modified Mathlib/RepresentationTheory/Basic.lean

deleted theorem Representation.apply_eq_self

added theorem Representation.isTrivial_apply

added theorem Representation.isTrivial_def

added theorem Representation.trivial_apply

deleted theorem Representation.trivial_def

Modified Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

Modified Mathlib/RepresentationTheory/Invariants.lean

Modified Mathlib/RepresentationTheory/Rep.lean

deleted def Rep.trivial

modified theorem Rep.trivial_def