exists_restrict_to_vars — Mathlib

English

If F is a polynomial with vars contained in s, there exists f on s such that evaluating f on restricted inputs recovers F.

Русский

Если F — полином с переменными, входящими в s, существует функция f на s такая, что при оценке на ограниченных входах мы восстанавливаем F.

LaTeX

$$$$ \exists f:(s \to R) \to R,\ \forall x:\sigma \to R,\ f(x|_s) = \mathrm{aeval}_x F $$$$

Lean4

theorem exists_restrict_to_vars (R : Type*) [CommRing R] {F : MvPolynomial σ ℤ} (hF : ↑F.vars ⊆ s) :
    ∃ f : (s → R) → R, ∀ x : σ → R, f (x ∘ (↑) : s → R) = aeval x F :=
  by
  rw [← mem_supported, supported_eq_range_rename, AlgHom.mem_range] at hF
  obtain ⟨F', hF'⟩ := hF
  use fun z ↦ aeval z F'
  intro x
  simp only [← hF', aeval_rename]

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