weightedHomogeneousComponent_eq_zero

English

If the weighted total degree of φ is less than n, then the n-th weighted homogeneous component is zero.

Русский

Если взвешенная общая степень φ меньше n, тогда n-я взвешенная однородная компонента равна нулю.

LaTeX

$$$weightedHomogeneousComponent\, w\, n\, φ = 0 \quad\text{whenever}\quad weightedTotalDegree\, w\, φ < n$$$

Lean4

theorem weightedHomogeneousComponent_eq_zero [SemilatticeSup M] [OrderBot M] (h : weightedTotalDegree w φ < n) :
    weightedHomogeneousComponent w n φ = 0 := by
  classical
  rw [weightedHomogeneousComponent_apply, sum_eq_zero]
  intro d hd
  rw [Finset.mem_filter] at hd
  exfalso
  apply lt_irrefl n
  nth_rw 1 [← hd.2]
  exact lt_of_le_of_lt (le_weightedTotalDegree w hd.1) h

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