Pointwise instances on
This file provides:
and the actions
which matches the action of
These are all available in the
Additionally, it provides various degrees of monoid structure:
AddSubmonoid.monoidwhich is available globally to match the monoid structure implied by
Implementation notes #
Most of the lemmas in this file are direct copies of lemmas from
While the statements of these lemmas are defeq, we repeat them here due to them not being
syntactically equal. Before adding new lemmas here, consider if they would also apply to the action
Some lemmas about pointwise multiplication and submonoids. Ideally we put these in
GroupTheory.Submonoid.Basic, but currently we cannot because that file is imported by this.
The action on an additive submonoid corresponding to applying the action to every element.
This is available as an instance in the
Elementwise monoid structure of additive submonoids #
These definitions are a cut-down versions of the ones around
Submodule.mul, as that API is
usually more useful.