Pointwise instances on
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file provides the action
subring.pointwise_mul_action which matches the action of
This actions is available in the
Implementation notes #
This file is almost identical to
ring_theory/subsemiring/pointwise.lean. Where possible, try to
keep them in sync.
The action on a subring corresponding to applying the action to every element.
This is available as an instance in the
equiv_smul like we have for subgroup.