English
The multiplicative action on affine subspaces is defined by applying the action to every point, i.e., a • s = s.map (DistribMulAction.toLinearMap k _ a).toAffineMap.
Русский
Умножение на подпроизведение действует поэлементно: a • s = s.map (DistribMulAction.toLinearMap k _ a).toAffineMap.
LaTeX
$$$ a \\cdot s = s.map\\bigl( (\\mathrm{DistribMulAction.toLinearMap}\\ k\\ V\\ a).toAffineMap \\bigr)$$$
Lean4
/-- The multiplicative action on an affine subspace corresponding to applying the action to every
element.
This is available as an instance in the `Pointwise` locale.
TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineSubspace k P)`, which acts on `P` with a
`VAdd` version of a `DistribMulAction`. -/
protected def mulAction : MulAction M (AffineSubspace k V) :=
SetLike.coe_injective.mulAction _ coe_smul
