degree_degLexDegree — Mathlib

English

For any multivariate polynomial f over a commutative semiring, the degree of f with respect to the degLex ordering, when interpreted as a natural degree, equals the total degree of f.

Русский

Для многочлена f по нескольким переменным над коммутативным полем, степень f относительно порядка degLex, взятая как натуральная степень, равна полной степени f.

LaTeX

$$$(\\degLex.degree\, f).degree = f.totalDegree$$$

Lean4

theorem degree_degLexDegree : (degLex.degree f).degree = f.totalDegree :=
  by
  by_cases hf : f = 0
  · simp [hf]
  apply le_antisymm
  · exact le_totalDegree (degLex.degree_mem_support hf)
  · unfold MvPolynomial.totalDegree
    apply Finset.sup_le
    intro b hb
    exact DegLex.monotone_degree (degLex.le_degree hb)

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