instModule — Mathlib

English

The space of affine maps to an R-module is itself an R-module, with the obvious pointwise operations derived from the base module structure.

Русский

Пространство аффинных отображений в R-модуль само образует R-модуль с очевидными покомпонентными операциями, полученными из базовой структуры модуля.

LaTeX

$$AffineMap.instModule : Module R (P1 →ᵃ[k] V2)$$

Lean4

/-- The space of affine maps taking values in an `R`-module is an `R`-module. -/
instance : Module R (P1 →ᵃ[k] V2) :=
  { AffineMap.distribMulAction with
    add_smul := fun _ _ _ => ext fun _ => add_smul _ _ _
    zero_smul := fun _ => ext fun _ => zero_smul _ _ }

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