coeFnLinearMap — Mathlib

English

The space of ContMDiffMap with a target V is a module over 𝕜.

Русский

Для натуральных степеней и целочисленного преобразования сохраняются кольцевые и аддитивные структуры на пространствах C^n-отображений.

LaTeX

$$Module 𝕜 ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n$$

Lean4

/-- Coercion to a function as a `LinearMap`. -/
@[simps]
def coeFnLinearMap {V : Type*} [NormedAddCommGroup V] [NormedSpace 𝕜 V] : C^n⟮I, N; 𝓘(𝕜, V), V⟯ →ₗ[𝕜] N → V :=
  {
    (coeFnAddMonoidHom : C^n⟮I, N; 𝓘(𝕜, V), V⟯ →+ _) with
    toFun := (↑)
    map_smul' := coe_smul }

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