Pointwise instances on
This file provides the action
subsemiring.pointwise_mul_action which matches the action of
This actions is available in the
Implementation notes #
This file is almost identical to
group_theory/submonoid/pointwise.lean. Where possible, try to
keep them in sync.
The action on a subsemiring corresponding to applying the action to every element.
This is available as an instance in the
equiv_smul like we have for subgroup.