weighted_total_degree — Mathlib

English

If φ is nonzero and weighted homogeneous of degree n, then its non-bottom weighted total degree equals n.

Русский

Если φ не нулевой и взвешенно однороден степени n, то его weightedTotalDegree' равна n.

LaTeX

$$weightedTotalDegree' w φ = n$$

Lean4

/-- A nonzero weighted-homogeneous polynomial of weighted degree `n` has weighted total degree
  `n`. -/
theorem weighted_total_degree [SemilatticeSup M] {w : σ → M} (hφ : IsWeightedHomogeneous w φ n) (h : φ ≠ 0) :
    weightedTotalDegree' w φ = n := by
  simp only [weightedTotalDegree']
  apply le_antisymm
  · simp only [Finset.sup_le_iff, mem_support_iff, WithBot.coe_le_coe]
    exact fun d hd => le_of_eq (hφ hd)
  · obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero h
    simp only [← hφ hd]
    replace hd := Finsupp.mem_support_iff.mpr hd
    apply Finset.le_sup hd

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