Documentation

Mathlib.Algebra.GroupWithZero.Action.Opposite

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:

Actions on the opposite type #

Actions on the opposite type just act on the underlying type.

Equations
Equations
Equations
Equations
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.

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

Equations
  • =