eval_mvPolynomial — Mathlib

English

Let Fintype σ and p ∈ MvPolynomial(σ, 𝕜). Then the map x ↦ eval(x) p is analytic on the whole space (Set.univ).

Русский

Пусть σ конечен, p ∈ MvPolynomial(σ, 𝕜). Тогда отображение x ↦ eval(x) p аналитично на всем пространстве.

LaTeX

$$$[Fintype\\, \\sigma]\\ (p:\\, MvPolynomial\\, \\sigma\\, 𝕜)\\; AnalyticOnNhd\\, 𝕜(\\, x \\mapsto \\operatorname{eval}(x, p)\\, )\\ Set.univ.$$$

Lean4

theorem eval_mvPolynomial [Fintype σ] (p : MvPolynomial σ 𝕜) : AnalyticOnNhd 𝕜 (eval · p) Set.univ :=
  AnalyticOnNhd.eval_linearMap (.id (R := 𝕜) (M := σ → 𝕜)) p

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