Mathlib Changelog
v4
Changelog
About
Github
Theorem
Representation.ofMulActionSubsingletonEquivTrivial_apply
Modification history
2026-03-09 18:39
Mathlib/RepresentationTheory/Equiv.lean
feat(RepresentationTheory/Action): Create representation from Action, second step of refactor Rep (#36341)
Added
Representation.ofMulActionSubsingletonEquivTrivial_apply
View on Github →