Commit 2024-01-22 15:15 6d0b012d

View on Github →

chore(RepresentationTheory/Action): Factor out constructors for Action V G from MulAction G X (#9662) Further splits Mathlib.RepresentationTheory.Action.Basic and factors out the construction of objects of Action V G from a MulAction G X instance.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RepresentationTheory/Action/Basic.lean

deleted def Action.diagonal

deleted def Action.diagonalOneIsoLeftRegular

deleted def Action.leftRegular

deleted def Action.ofMulAction

deleted def Action.ofMulActionLimitCone

deleted theorem Action.ofMulAction_apply

Created Mathlib/RepresentationTheory/Action/Concrete.lean

added def Action.diagonal

added def Action.diagonalOneIsoLeftRegular

added def Action.leftRegular

added def Action.ofMulAction

added def Action.ofMulActionLimitCone

added theorem Action.ofMulAction_apply

Modified Mathlib/RepresentationTheory/Action/Monoidal.lean