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.instSMulMulOpposite
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.
Equations
- (_ : VAddAssocClass M N αᵃᵒᵖ) = (_ : VAddAssocClass M N αᵃᵒᵖ)
Equations
- (_ : VAddCommClass M N αᵃᵒᵖ) = (_ : VAddCommClass M N αᵃᵒᵖ)
Equations
- (_ : IsCentralVAdd R αᵃᵒᵖ) = (_ : IsCentralVAdd R αᵃᵒᵖ)
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
.
Equations
- Add.toHasOppositeVAdd α = { vadd := fun c x => x + c.unop }
Like Mul.toSMul
, but multiplies on the right.
See also Monoid.toOppositeMulAction
and MonoidWithZero.toOppositeMulActionWithZero
.
Equations
- Mul.toHasOppositeSMul α = { smul := fun c x => x * c.unop }
Equations
- (_ : AddAction.IsPretransitive Gᵃᵒᵖ G) = (_ : AddAction.IsPretransitive Gᵃᵒᵖ G)
The right regular action of an additive group on itself is transitive.
The right regular action of a group on itself is transitive.
Equations
- (_ : VAddCommClass αᵃᵒᵖ α α) = (_ : VAddCommClass αᵃᵒᵖ α α)
Equations
- (_ : VAddCommClass α αᵃᵒᵖ α) = (_ : VAddCommClass α αᵃᵒᵖ α)
Equations
- (_ : IsCentralVAdd α α) = (_ : IsCentralVAdd α α)
Like AddMonoid.toAddAction
, but adds on the right.
Like Monoid.toMulAction
, but multiplies on the right.
Equations
- (_ : VAddAssocClass M Nᵃᵒᵖ N) = (_ : VAddAssocClass M Nᵃᵒᵖ N)
Equations
- (_ : VAddCommClass M Nᵃᵒᵖ N) = (_ : VAddCommClass M Nᵃᵒᵖ N)
AddMonoid.toOppositeAddAction
is faithful on cancellative monoids.
Equations
- (_ : FaithfulVAdd αᵃᵒᵖ α) = (_ : FaithfulVAdd αᵃᵒᵖ α)
Monoid.toOppositeMulAction
is faithful on cancellative monoids.
Monoid.toOppositeMulAction
is faithful on nontrivial cancellative monoids with zero.