coeff_eq_zero_of_totalDegree_lt — Mathlib

English

Renaming variables does not increase total degree: the total degree of the renamed polynomial is at most the original total degree.

Русский

Переименование переменных не увеличивает общую степень: общая степень переименованного полинома не превосходит исходной степени.

LaTeX

$$$\\\\forall f : MvPolynomial σ R, \\\\forall (f' : σ \\\\to σ), \\\\ totalDegree(rename f f') \\\\le totalDegree f$$$

Lean4

theorem coeff_eq_zero_of_totalDegree_lt {f : MvPolynomial σ R} {d : σ →₀ ℕ} (h : f.totalDegree < ∑ i ∈ d.support, d i) :
    coeff d f = 0 := by
  classical
  rw [totalDegree, Finset.sup_lt_iff] at h
  · specialize h d
    rw [mem_support_iff] at h
    refine not_not.mp (mt h ?_)
    exact lt_irrefl _
  · exact lt_of_le_of_lt (Nat.zero_le _) h

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