weightedHomogeneousComponent_isWeightedHomogeneous

English

The n-th weighted homogeneous component of φ is weighted homogeneous of degree n with respect to w.

Русский

Компонента φ взвешенная по n является взвешенно однородной степенью n относительно w.

LaTeX

$$$IsWeightedHomogeneous\, w\, n\, (weightedHomogeneousComponent\, w\, n\, \varphi)$$$

Lean4

/-- The `n` weighted homogeneous component of a polynomial is weighted homogeneous of
weighted degree `n`. -/
theorem weightedHomogeneousComponent_isWeightedHomogeneous :
    (weightedHomogeneousComponent w n φ).IsWeightedHomogeneous w n := by
  classical
  intro d hd
  contrapose! hd
  rw [coeff_weightedHomogeneousComponent, if_neg hd]

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