English
The constant coefficient map is surjective: every r ∈ R appears as the constant term of some power series.
Русский
Обратимая к константному коэффициенту карта полна образом: любой элемент R является константным коэффициентом некоторого ряда.
LaTeX
$$$\\forall R\\ [\\operatorname{Semiring} R],\\ \\operatorname{constantCoeff}: R\\llbracket X\\rrbracket \\to R \\text{ is surjective, i.e. } \\forall r \\in R, \\exists \\phi \\in R\\llbracket X\\rrbracket, \\operatorname{constantCoeff}(\\phi) = r$$$
Lean4
theorem constantCoeff_surj : Function.Surjective (constantCoeff (R := R)) := fun r =>
⟨C r, constantCoeff_C r⟩
-- The following section duplicates the API of `Mathlib.Data.Polynomial.Coeff` and should attempt
-- to keep up to date with that
