evalᵢ — Mathlib

English

Evaluation in the restricted degree setting: eval_i is the K-linear map whose action satisfies eval_i(p)(e) = eval(e, p) for p ∈ R(σ, K) and e ∈ σ → K.

Русский

Оценивание в рамках ограниченной степени: eval_i — это K-линейное отображение, такое что для p ∈ R(σ, K) и e ∈ σ → K выполняется eval_i(p)(e) = eval(e, p).

LaTeX

$$$\\\\mathrm{eval}_i(p)(e) = \\\\mathrm{eval}(e, p) \\quad (p \\in R(\\\\sigma, K), \\ e \\in (\\\\sigma \\to K)).$$$

Lean4

/-- Evaluation in the `MvPolynomial.R` subtype. -/
noncomputable def evalᵢ [CommRing K] : R σ K →ₗ[K] (σ → K) → K :=
  (evalₗ K σ).comp (restrictDegree σ K (Fintype.card K - 1)).subtype

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