weightedHomogeneousComponent_eq_zero_of_notMem

English

Same as 181033: if i is not in the image of weight w on φ.support, then the i-th component is zero.

Русский

То же, что и 181033.

LaTeX

$$$i \notin \operatorname{image}(weight\, w)\; \varphi.support \Rightarrow weightedHomogeneousComponent\, w\, i\, \varphi = 0$$$

Lean4

theorem weightedHomogeneousComponent_eq_zero_of_notMem [DecidableEq M] (φ : MvPolynomial σ R) (i : M)
    (hi : i ∉ Finset.image (weight w) φ.support) : weightedHomogeneousComponent w i φ = 0 :=
  by
  apply weightedHomogeneousComponent_eq_zero'
  simp only [Finset.mem_image, mem_support_iff, ne_eq, not_exists, not_and] at hi
  exact fun m hm ↦ hi m (mem_support_iff.mp hm)

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