lcoeff — Mathlib

English

For fixed m, lcoeff m is the R-linear map from MvPolynomial σ R to R given by p ↦ coeff m p.

Русский

Для фиксированного m отображение lcoeff m является линейным по модулю R от MvPolynomial σ R в R, заданное как p ↦ coeff m p.

LaTeX

$$$l_{m}: MvPolynomial\;\sigma\;R \to_{\text{linear}} R\quad\text{with}\quad l_{m}(p)=\mathrm{coeff}\;m\;p$$$

Lean4

/-- `MvPolynomial.coeff m` but promoted to a `LinearMap`. -/
@[simps]
def lcoeff (m : σ →₀ ℕ) : MvPolynomial σ R →ₗ[R] R
    where
  toFun := coeff m
  map_add' := coeff_add m
  map_smul' := coeff_smul m

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