weightedHomogeneousComponent_eq_zero'

English

If every monomial of φ has weight not equal to n, then the n-th weighted homogeneous component is zero.

Русский

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

LaTeX

$$ (∀ d, d ∈ \operatorname{supp}(φ) ⇒ weight(w)\, d ≠ n) → weightedHomogeneousComponent\, w\, n\, φ = 0$$

Lean4

theorem weightedHomogeneousComponent_eq_zero' (h : ∀ d : σ →₀ ℕ, d ∈ φ.support → weight w d ≠ n) :
    weightedHomogeneousComponent w n φ = 0 := by
  classical
  rw [weightedHomogeneousComponent_apply, sum_eq_zero]
  intro d hd; rw [mem_filter] at hd
  exfalso; exact h _ hd.1 hd.2

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