homogeneousComponent_zero — Mathlib

English

If for every degree-exponent d ∈ φ.support one has d.degree ≠ n, then homogeneousComponent(n) φ = 0.

Русский

Если для каждого d ∈ support φ выполняется d.degree ≠ n, то homogeneousComponent(n) φ = 0.

LaTeX

$$∀ d ∈ φ.support, d.degree ≠ n ⇒ homogeneousComponent(n) φ = 0$$

Lean4

@[simp]
theorem homogeneousComponent_zero : homogeneousComponent 0 φ = C (coeff 0 φ) :=
  weightedHomogeneousComponent_zero φ (fun _ => Nat.succ_ne_zero Nat.zero)

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