coeffAddMonoidHom — Mathlib

English

For a fixed m, the map p ↦ coeff m p defines an additive monoid hom from MvPolynomial σ R to R.

Русский

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

LaTeX

$$$\exists h:\mathrm{MvPolynomial}\;\sigma\;R \to+ R\text{ such that }\forall p, h(p)=\mathrm{coeff}\;m\;p$$$

Lean4

/-- `MvPolynomial.coeff m` but promoted to an `AddMonoidHom`. -/
@[simps]
def coeffAddMonoidHom (m : σ →₀ ℕ) : MvPolynomial σ R →+ R
    where
  toFun := coeff m
  map_zero' := coeff_zero m
  map_add' := coeff_add m

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