isWeightedHomogeneous_weightedHomogeneousComponent

English

The weighted homogeneous component map is weighted homogeneous of the same weight p, i.e., applying the component after codomain preserves the weight.

Русский

Произведение весовых однородных компонент сохраняет вес p.

LaTeX

$$$ is\_weighted\_homogeneous\ w\ p (weightedHomogeneousComponent\ w\ p) \text{ is weighted homogeneous of weight } p $$$

Lean4

theorem isWeightedHomogeneous_weightedHomogeneousComponent (f : MvPowerSeries σ R) (p : ℕ) :
    IsWeightedHomogeneous w (f.weightedHomogeneousComponent w p) p := fun {d} ↦
  by
  rw [not_imp_comm]
  intro hd
  rw [coeff_weightedHomogeneousComponent, if_neg hd]

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