C_surjective — Mathlib

English

Every multivariate polynomial is a constant polynomial image of some coefficient.

Русский

Любой многочлен является образом константного полинома от некоторого коэффициента.

LaTeX

$$$ \forall p:\, MvPolynomial\; \sigma\; R, \exists a:\, R,\ C\ a = p $$$

Lean4

theorem C_surjective {R : Type*} [CommSemiring R] (σ : Type*) [IsEmpty σ] :
    Function.Surjective (C : R → MvPolynomial σ R) :=
  by
  refine fun p => ⟨p.toFun 0, Finsupp.ext fun a => ?_⟩
  simp only [C_apply, ← single_eq_monomial, (Finsupp.ext isEmptyElim (α := σ) : a = 0), single_eq_same]
  rfl

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