weightedHomogeneousComponent_ne — Mathlib

English

If p is weighted homogeneous of degree m and n ≠ m, then the n-th component is zero.

Русский

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

LaTeX

$$$IsWeightedHomogeneous\, w\, p\, m \Rightarrow n \neq m \Rightarrow weightedHomogeneousComponent\, w\, n\, p = 0$$$

Lean4

theorem weightedHomogeneousComponent_ne {m : M} (n : M) {p : MvPolynomial σ R} (hp : IsWeightedHomogeneous w p m) :
    n ≠ m → weightedHomogeneousComponent w n p = 0 := by
  classical
  intro hn
  ext x
  rw [coeff_weightedHomogeneousComponent]
  by_cases zero_coeff : coeff x p = 0
  · simp [zero_coeff]
  · rw [if_neg]
    · rw [coeff_zero]
    · rw [hp zero_coeff]; exact Ne.symm hn

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