English
Let f be a nonzero multivariate polynomial in n+1 variables. Under the finSuccEquiv transformation, the total degree of the transformed polynomial equals the degree of f with respect to the first (0-th) variable.
Русский
Пусть f ненулевой многочлен в n+1 переменных. При преобразовании finSuccEquiv общая степень полученного многочлена равна степени f по первой (нулевой) переменной.
LaTeX
$$$\deg\bigl(\mathrm{finSuccEquiv}(R,n)\,f\bigr) = \deg_0 f$$$
Lean4
theorem degree_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) :
(finSuccEquiv R n f).degree = degreeOf 0 f := by
-- TODO: these should be lemmas
have h₀ : ∀ {α β : Type _} (f : α → β), (fun x => x) ∘ f = f := fun f => rfl
have h₁ : ∀ {α β : Type _} (f : α → β), f ∘ (fun x => x) = f := fun f => rfl
have h' : ((finSuccEquiv R n f).support.sup fun x => x) = degreeOf 0 f := by
rw [degreeOf_eq_sup, support_finSuccEquiv, Finset.sup_image, h₀]
rw [Polynomial.degree, ← h', Nat.cast_withBot, Finset.coe_sup_of_nonempty (support_finSuccEquiv_nonempty h),
Finset.max_eq_sup_coe, h₁]
