Pointwise instances on Submodule
s #
This file provides:
and the actions
which matches the action of Set.mulActionSet
.
These actions are available in the Pointwise
locale.
Implementation notes #
Most of the lemmas in this file are direct copies of lemmas from
GroupTheory/Submonoid/Pointwise.lean
.
The submodule with every element negated. Note if R
is a ring and not just a semiring, this
is a no-op, as shown by Submodule.neg_eq_self
.
Recall that When R
is the semiring corresponding to the nonnegative elements of R'
,
Submodule R' M
is the type of cones of M
. This instance reflects such cones about 0
.
This is available as an instance in the Pointwise
locale.
Instances For
Submodule.pointwiseNeg
is involutive.
This is available as an instance in the Pointwise
locale.
Instances For
Submodule.pointwiseNeg
as an order isomorphism.
Instances For
The action on a submodule corresponding to applying the action to every element.
This is available as an instance in the Pointwise
locale.
Instances For
See also Submodule.smul_bot
.
See also Submodule.smul_sup
.
The action on a submodule corresponding to applying the action to every element.
This is available as an instance in the Pointwise
locale.
This is a stronger version of Submodule.pointwiseDistribMulAction
. Note that add_smul
does
not hold so this cannot be stated as a Module
.