IsWeightedHomogeneous — Mathlib

English

A power series is weighted homogeneous of weight p if all its nonzero coefficients lie on the same weight level p with respect to a given weight function w.

Русский

Степенной ряд является взвешенно однородным по весу p, если все ненулевые коэффициенты лежат на одном весовом уровне p по заданной функции весов w.

LaTeX

$$$ \text{IsWeightedHomogeneous}(f,p) \iff \forall d, \ f_{d} \neq 0 \Rightarrow w(d) = p $$$

Lean4

/-- Weighted homogeneous power series -/
def IsWeightedHomogeneous (f : MvPowerSeries σ R) (p : ℕ) : Prop :=
  ∀ {d : σ →₀ ℕ}, f.coeff d ≠ 0 → weight w d = p

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