English
The space of affine maps to a module carries an action by a ring R, turning it into an R-module via the codomain action.
Русский
Пространство аффинных отображений в модуль имеет действие кольца R, превращающее его в модуль над R через действие кодом.
LaTeX
$$AffineMap.distribMulAction : DistribMulAction R (P1 →ᵃ[k] V2)$$
Lean4
/-- The space of affine maps to a module inherits an `R`-action from the action on its codomain. -/
instance distribMulAction : DistribMulAction R (P1 →ᵃ[k] V2)
where
smul_add _ _ _ := ext fun _ => smul_add _ _ _
smul_zero _ := ext fun _ => smul_zero _