isHomogeneous_iff_eq_homogeneousComponent

English

A function f is homogeneous of degree p if and only if f equals its p-th homogeneous component.

Русский

Функция f однородна степени p тогда и только тогда, когда она равна своей p-й однородной компоненте.

LaTeX

$$IsHomogeneous(f, p) ↔ f = f.homogeneousComponent(p)$$

Lean4

theorem isHomogeneous_iff_eq_homogeneousComponent {f : MvPowerSeries σ R} {p : ℕ} :
    IsHomogeneous f p ↔ f = f.homogeneousComponent p :=
  isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent

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