English
For the coefficients of finSuccEquiv, the j-th degree (in the j-succ variable) of the i-th coefficient is bounded by the degree of the original polynomial in the successor variable.
Русский
Для коэффициентов finSuccEquiv степень j-го коэффициента по переменной j-следующей ограничена степенью исходного полинома по переменной successor.
LaTeX
$$$\deg_j\bigl(\mathrm{coeff}(\mathrm{finSuccEquiv}(R,n)\,p)_i\bigr) \le \deg_{j\!\!\text{succ}} p$$$
Lean4
theorem degreeOf_coeff_finSuccEquiv (p : MvPolynomial (Fin (n + 1)) R) (j : Fin n) (i : ℕ) :
degreeOf j (Polynomial.coeff (finSuccEquiv R n p) i) ≤ degreeOf j.succ p :=
by
rw [degreeOf_eq_sup, degreeOf_eq_sup, Finset.sup_le_iff]
intro m hm
rw [← Finsupp.cons_succ j i m]
exact Finset.le_sup (f := fun (g : Fin (Nat.succ n) →₀ ℕ) => g (Fin.succ j)) (support_coeff_finSuccEquiv.1 hm)
