coeff_eq_zero — Mathlib

English

If p equals the weighted order of f, then the weighted homogeneous component of weight p of f is nonzero.

Русский

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

LaTeX

$$$ p = f.weightedOrder\, w \Rightarrow f.weightedHomogeneousComponent\, w\, p \neq 0 $$$

Lean4

theorem coeff_eq_zero {f : MvPowerSeries σ R} {p : ℕ} (hf : f.IsWeightedHomogeneous w p) {d : σ →₀ ℕ}
    (hd : weight w d ≠ p) : f.coeff d = 0 := by simpa [Classical.not_not] using mt (@hf d) hd

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