constantCoeff_surjective — Mathlib

English

Every element x of R is the constant term of some polynomial; in fact, constantCoeff(C x) = x, where C x is the constant polynomial with value x.

Русский

Каждый элемент x в R является константный членом некоторого многочлена; например, constantCoeff(C x) = x, где C x — константный многочлен со значением x.

LaTeX

$$$\forall x \in R, \exists p \in R[X], \operatorname{constantCoeff}(p) = x$. Equivalently, $\operatorname{coeff}(C x, 0) = x$.$$

Lean4

theorem constantCoeff_surjective : Function.Surjective (constantCoeff (R := R)) := fun x ↦ ⟨C x, by simp⟩

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