distribMulAction — Mathlib

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 _

Похожие утверждения