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 forr • m
m <• r
as an alias forMulOpposite.op r • m
v +ᵥ> p
as an alias forv +ᵥ p
p <+ᵥ v
as an alias forAddOpposite.op v +ᵥ p
Actions on the opposite type #
Actions on the opposite type just act on the underlying type.
Right actions #
In this section we establish SMul αᵐᵒᵖ β
as the canonical spelling of right scalar multiplication
of β
by α
, and provide convenient notations.
Pretty printer defined by notation3
command.
Equations
Instances For
With open scoped RightActions
, an alternative symbol for left actions, r • m
.
In lemma names this is still called smul
.
Equations
Instances For
With open scoped RightActions
, a shorthand for right actions, op r • m
.
In lemma names this is still called op_smul
.
Equations
Instances For
Pretty printer defined by notation3
command.
Equations
Instances For
With open scoped RightActions
, an alternative symbol for left actions, r • m
.
In lemma names this is still called vadd
.
Equations
Instances For
Pretty printer defined by notation3
command.
Equations
Instances For
With open scoped RightActions
, a shorthand for right actions, op r +ᵥ m
.
In lemma names this is still called op_vadd
.
Equations
Instances For
Pretty printer defined by notation3
command.
Equations
Instances For
Actions by the opposite type (right actions) #
Like Monoid.toMulAction
, but multiplies on the right.
Equations
Like AddMonoid.toAddAction
, but adds on the right.