English
The constantCoeff map from polynomials to the base ring R assigns to each polynomial its constant term, i.e., constantCoeff(p) = coeff p 0; this is a ring homomorphism.
Русский
Отображение constantCoeff из многочленов в базовую кольцо R возвращает их константный член, то есть constantCoeff(p) = coeff(p,0); это гомоморфизм кольца.
LaTeX
$$$\text{constantCoeff}: R[X] \to R, \quad \text{constantCoeff}(p) = \operatorname{coeff}(p,0)$$$
Lean4
/-- `constantCoeff p` returns the constant term of the polynomial `p`,
defined as `coeff p 0`. This is a ring homomorphism. -/
@[simps]
def constantCoeff : R[X] →+* R where
toFun p := coeff p 0
map_one' := coeff_one_zero
map_mul' := mul_coeff_zero
map_zero' := coeff_zero 0
map_add' p q := coeff_add p q 0
