Def Action.diagonalOneIsoLeftRegular
Modification history
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 →