constantCoeff — Mathlib

English

The constantCoeff map equals the 0-th coefficient map: constantCoeff = coeff 0.

Русский

Постоянная коэффициента равна коэффициенту при нуле: constantCoeff = coeff 0.

LaTeX

$$$ constantCoeff = coeff 0. $$$

Lean4

/-- `constantCoeff p` returns the constant term of the polynomial `p`, defined as `coeff 0 p`.
This is a ring homomorphism.
-/
def constantCoeff : MvPolynomial σ R →+* R where
  toFun := coeff 0
  map_one' := by simp
  map_mul' := by classical simp [coeff_mul]
  map_zero' := coeff_zero _
  map_add' := coeff_add _

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