natDegree_finSuccEquiv — Mathlib

English

For any polynomial f in Fin(n+1), the natural degree of its finSuccEquiv image equals the degree of f with respect to the 0-th variable.

Русский

Для любого полинома f в Fin(n+1) натуральная степень образа под finSuccEquiv равна степени f по 0-й переменной.

LaTeX

$$$\mathrm{natDegree}(\mathrm{finSuccEquiv}(R,n)\,f) = \deg_0 f$$$

Lean4

theorem natDegree_finSuccEquiv (f : MvPolynomial (Fin (n + 1)) R) : (finSuccEquiv R n f).natDegree = degreeOf 0 f :=
  by
  by_cases c : f = 0
  · rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]
  · rw [Polynomial.natDegree, degree_finSuccEquiv c, Nat.cast_withBot, WithBot.unbotD_coe]

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