Scalar actions on and by Mᵐᵒᵖ #
This file defines the actions on the opposite type SMul R Mᵐᵒᵖ, and actions by the opposite
type, SMul Rᵐᵒᵖ M.
Note that MulOpposite.smul is provided in an earlier file as it is needed to
provide the AddMonoid.nsmul and AddCommGroup.zsmul fields.
Notation #
With open scoped RightActions, this provides:
r •> mas an alias forr • mm <• ras an alias forMulOpposite.op r • mv +ᵥ> pas an alias forv +ᵥ pp <+ᵥ vas an alias forAddOpposite.op v +ᵥ p
Actions on the opposite type #
Actions on the opposite type just act on the underlying type.
instance
MulOpposite.instSMulZeroClass
{M : Type u_1}
{α : Type u_2}
[AddMonoid α]
[SMulZeroClass M α]
:
SMulZeroClass M αᵐᵒᵖ
Equations
instance
MulOpposite.instSMulWithZero
{M : Type u_1}
{α : Type u_2}
[MonoidWithZero M]
[AddMonoid α]
[SMulWithZero M α]
:
SMulWithZero M αᵐᵒᵖ
Equations
instance
MulOpposite.instMulActionWithZero
{M : Type u_1}
{α : Type u_2}
[MonoidWithZero M]
[AddMonoid α]
[MulActionWithZero M α]
:
Equations
instance
MulOpposite.instDistribMulAction
{M : Type u_1}
{α : Type u_2}
[Monoid M]
[AddMonoid α]
[DistribMulAction M α]
:
Equations
instance
MulOpposite.instMulDistribMulAction
{M : Type u_1}
{α : Type u_2}
[Monoid M]
[Monoid α]
[MulDistribMulAction M α]
:
Equations
Actions by the opposite type (right actions) #
In Mul.toSMul in another file, we define the left action a₁ • a₂ = a₁ * a₂. For the
multiplicative opposite, we define MulOpposite.op a₁ • a₂ = a₂ * a₁, with the multiplication
reversed.
instance
CancelMonoidWithZero.toFaithfulSMul_opposite
{α : Type u_2}
[CancelMonoidWithZero α]
[Nontrivial α]
:
FaithfulSMul αᵐᵒᵖ α
Monoid.toOppositeMulAction is faithful on nontrivial cancellative monoids with zero.