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