isWeightedHomogeneous_of_total_degree_zero

English

If a polynomial is of total degree ⊥, then it is weighted homogeneous of degree ⊥.

Русский

Если полином имеет общую нуль-степень, то он взвешенно однороден степени ⊥.

LaTeX

$$IsWeightedHomogeneous w p ⊥ if weightedTotalDegree w p = ⊥$$

Lean4

/-- A polynomial of weightedTotalDegree `⊥` is weighted_homogeneous of degree `⊥`. -/
theorem isWeightedHomogeneous_of_total_degree_zero [SemilatticeSup M] [OrderBot M] (w : σ → M) {p : MvPolynomial σ R}
    (hp : weightedTotalDegree w p = (⊥ : M)) : IsWeightedHomogeneous w p (⊥ : M) :=
  by
  intro d hd
  have h := weightedTotalDegree_coe w p (MvPolynomial.ne_zero_iff.mpr ⟨d, hd⟩)
  simp only [weightedTotalDegree', hp] at h
  rw [eq_bot_iff, ← WithBot.coe_le_coe, ← h]
  apply Finset.le_sup (mem_support_iff.mpr hd)

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