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 •> m as an alias for r • m
• m <• r as an alias for MulOpposite.op r • m
• v +ᵥ> p as an alias for v +ᵥ p
• p <+ᵥ v as an alias for AddOpposite.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

• MulOpposite.instSMulZeroClass = SMulZeroClass.mk ⋯

instance MulOpposite.instSMulWithZero {M : Type u_1} {α : Type u_2} [MonoidWithZero M] [AddMonoid α] [SMulWithZero M α] : SMulWithZero M αᵐᵒᵖ

Equations

• MulOpposite.instSMulWithZero = SMulWithZero.mk ⋯

instance MulOpposite.instMulActionWithZero {M : Type u_1} {α : Type u_2} [MonoidWithZero M] [AddMonoid α] [MulActionWithZero M α] : MulActionWithZero M αᵐᵒᵖ

Equations

• MulOpposite.instMulActionWithZero = MulActionWithZero.mk ⋯ ⋯

instance MulOpposite.instDistribMulAction {M : Type u_1} {α : Type u_2} [Monoid M] [AddMonoid α] [DistribMulAction M α] : DistribMulAction M αᵐᵒᵖ

Equations

• MulOpposite.instDistribMulAction = DistribMulAction.mk ⋯ ⋯

instance MulOpposite.instMulDistribMulAction {M : Type u_1} {α : Type u_2} [Monoid M] [Monoid α] [MulDistribMulAction M α] : MulDistribMulAction M αᵐᵒᵖ

Equations

• MulOpposite.instMulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯

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.

theorem CancelMonoidWithZero.toFaithfulSMul_opposite {α : Type u_2} [CancelMonoidWithZero α] [Nontrivial α] : FaithfulSMul αᵐᵒᵖ α

Monoid.toOppositeMulAction is faithful on nontrivial cancellative monoids with zero.