weightedHomogeneousComponent_of_weightedOrder

English

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

Русский

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

LaTeX

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

Lean4

theorem weightedHomogeneousComponent_of_weightedOrder {f : MvPowerSeries σ R} {p : ℕ} (hf : p = f.weightedOrder w) :
    f.weightedHomogeneousComponent w p ≠ 0 := by
  intro hf'
  obtain ⟨d, hd⟩ := f.exists_coeff_ne_zero_and_weightedOrder w (by rw [← hf, toNat_coe])
  simp only [ne_eq, ← hf, Nat.cast_inj] at hd
  apply hd.1
  rw [MvPowerSeries.ext_iff] at hf'
  specialize hf' d
  simp only [coeff_weightedHomogeneousComponent, coeff_zero, ite_eq_right_iff] at hf'
  exact hf' hd.2

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