weightedHomogeneousComponent_same

English

If p is weighted homogeneous of degree m, then the m-th weighted homogeneous component of p is p itself.

Русский

Если p взвешенно однородный степени m, то m-я взвешенная однородная компонента p равна p.

LaTeX

$$$IsWeightedHomogeneous\, w\, p\, m \Rightarrow weightedHomogeneousComponent\, w\, m\, p = p$$$

Lean4

theorem weightedHomogeneousComponent_same {m : M} {p : MvPolynomial σ R} (hp : IsWeightedHomogeneous w p m) :
    weightedHomogeneousComponent w m p = p := by
  classical
  ext x
  rw [coeff_weightedHomogeneousComponent]
  by_cases zero_coeff : coeff x p = 0
  · split_ifs
    · rfl
    rw [zero_coeff]
  · rw [hp zero_coeff, if_pos rfl]

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