isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent

English

A power series is weighted homogeneous of weight p if and only if it equals its weight-p weighted homogeneous component.

Русский

Ряд взвешенно однороден по весу p тогда и только тогда, когда он равен своему весовому компоненту веса p.

LaTeX

$$$ \text{IsWeightedHomogeneous}\ w f p \iff f = f.weightedHomogeneousComponent\ w p $$$

Lean4

theorem isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent {f : MvPowerSeries σ R} {p : ℕ} :
    IsWeightedHomogeneous w f p ↔ f = f.weightedHomogeneousComponent w p :=
  by
  constructor
  · intro hf
    ext d
    rw [coeff_weightedHomogeneousComponent]
    split_ifs with hd
    · rfl
    · exact hf.coeff_eq_zero hd
  · intro hf
    rw [hf]
    exact isWeightedHomogeneous_weightedHomogeneousComponent w f p

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