THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file provides the additive action
affine_subspace.pointwise_add_action in the
The additive action on an affine subspace corresponding to applying the action to every element.
This is available as an instance in the