Def Action.diagonalOneIsoLeftRegular
Modification history
2025-05-02 13:41
Mathlib/CategoryTheory/Action/Concrete.lean
chore(CategoryTheory/Action): generalize universes (#24547) …
Modified Action.diagonalOneIsoLeftRegularView on Github →2024-01-22 15:15
Mathlib/RepresentationTheory/Action/Basic.lean
chore(RepresentationTheory/Action): Factor out constructors for `Action V G` from `MulAction G X` (#9662) …
Modified Action.diagonalOneIsoLeftRegularView on Github →