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.
Actions on the opposite type #
Actions on the opposite type just act on the underlying type.
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.
Like Add.toVAdd
, but adds on the right.
See also AddMonoid.to_OppositeAddAction
.
Like Mul.toSMul
, but multiplies on the right.
See also Monoid.toOppositeMulAction
and MonoidWithZero.toOppositeMulActionWithZero
.
The right regular action of an additive group on itself is transitive.
The right regular action of a group on itself is transitive.
Like AddMonoid.toAddAction
, but adds on the right.
Like Monoid.toMulAction
, but multiplies on the right.
AddMonoid.toOppositeAddAction
is faithful on cancellative monoids.
Monoid.toOppositeMulAction
is faithful on cancellative monoids.
Monoid.toOppositeMulAction
is faithful on nontrivial cancellative monoids with zero.