coeff_eq_zero — Mathlib

English

For a homogeneous power series of weight p, if the degree d is different from p, then the coefficient at d is zero.

Русский

Для однородного ряда веса p, если deg(d) ≠ p, то коэффициент при d равен 0.

LaTeX

$$$ f.IsHomogeneous p \rightarrow \forall d, d.weight \neq p \Rightarrow coeff_d f = 0 $$$

Lean4

theorem coeff_eq_zero {f : MvPowerSeries σ R} {p : ℕ} (hf : f.IsHomogeneous p) {d : σ →₀ ℕ} (hd : degree d ≠ p) :
    f.coeff d = 0 := by
  apply IsWeightedHomogeneous.coeff_eq_zero hf
  rwa [degree_eq_weight_one] at hd

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