English
In a finite-variable polynomial, under the same bound as above, for any exponent vector in the support there exists a coordinate less than n.
Русский
В конечном количестве переменных полином, при таком же ограничении, для любого вектора степеней в поддержке существует координата меньше n.
LaTeX
$$$\\\\forall f : MvPolynomial σ R,\\\\forall n : \\mathbb{N}, f.totalDegree < n * |σ| \\\\Rightarrow \\\\forall d \\\\in f.support, \\\\exists i \\\\in σ, \\\\ d i < n$$$
Lean4
theorem totalDegree_eq_zero_iff_eq_C {p : MvPolynomial σ R} : p.totalDegree = 0 ↔ p = C (p.coeff 0) :=
by
constructor <;> intro h
· ext m; classical rw [coeff_C]; split_ifs with hm; · rw [← hm]
apply coeff_eq_zero_of_totalDegree_lt; rw [h]
exact
Finset.sum_pos (fun i hi ↦ Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)
(Finsupp.support_nonempty_iff.mpr <| Ne.symm hm)
· rw [h, totalDegree_C]
