evalₗ — Mathlib

English

There is a natural K-linear map eval_ℓ from R(σ, K) to (σ → K) → K, defined by eval_ℓ(p)(e) = eval(e, p).

Русский

Существует естественное линейное по типу K отображение eval_ℓ: R(σ, K) → (σ → K) → K, определяемое как eval_ℓ(p)(e) = eval(e, p).

LaTeX

$$$\\\\mathrm{eval}_{\\\\ell}: R(\\\\sigma, K) \\\\to_K (\\\\sigma \\\\to K) \\\\to K, \\\\qquad \\\\mathrm{eval}_{\\\\ell}(p)(e) = \\mathrm{eval}(e, p).$$$

Lean4

/-- `MvPolynomial.eval` as a `K`-linear map. -/
@[simps]
def evalₗ [CommSemiring K] : MvPolynomial σ K →ₗ[K] (σ → K) → K
    where
  toFun p e := eval e p
  map_add' p q := by ext x; simp
  map_smul' a p := by ext e; simp

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