coeff_eq_zero — Mathlib

English

The projection extracting the degree-n weighted homogeneous component is linear; coefficients are preserved by restriction to the weight set.

Русский

Проекция, извлекающая компонент взвешенно однородной степени n, линейна; коэффициенты сохраняются при ограничении по весу.

LaTeX

$$coeff_weightedHomogeneousComponent w n φ$$

Lean4

/-- The weighted degree of a weighted homogeneous polynomial controls its support. -/
theorem coeff_eq_zero {w : σ → M} (hφ : IsWeightedHomogeneous w φ n) (d : σ →₀ ℕ) (hd : weight w d ≠ n) :
    coeff d φ = 0 := by
  have aux := mt (@hφ d) hd
  rwa [Classical.not_not] at aux

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