coeFnₗ — Mathlib

English

The map coeFnₗ is a linear map from LocallyConstant(X,Y) to X→Y, i.e., it is compatible with scalar multiplication and addition.

Русский

Карта coeFnₗ является линейным отображением от LocallyConstant(X,Y) к X→Y, то есть сохраняет суммацию и умножение на скаляры.

LaTeX

$$$\operatorname{coeFn}_{\ell}(R) : \operatorname{LocallyConstant}(X,Y) \to_{\ell} (X \to Y)$$$

Lean4

/-- `DFunLike.coe` as a linear map. -/
@[simps!]
def coeFnₗ (R : Type*) [Semiring R] [AddCommMonoid Y] [Module R Y] : LocallyConstant X Y →ₗ[R] X → Y
    where
  toAddHom := coeFnAddMonoidHom.toAddHom
  map_smul' _ _ := rfl

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