homogeneousComponent_eq_zero — Mathlib

English

If φ.totalDegree < n, then homogeneousComponent(n) φ = 0 (alternative formulation).

Русский

Если φ.totalDegree < n, то homogeneousComponent(n) φ = 0 (вариант формулировки).

LaTeX

$$φ.totalDegree < n ⇒ homogeneousComponent(n) φ = 0$$

Lean4

theorem homogeneousComponent_eq_zero (h : φ.totalDegree < n) : homogeneousComponent n φ = 0 :=
  by
  apply homogeneousComponent_eq_zero'
  rw [totalDegree, Finset.sup_lt_iff (lt_of_le_of_lt (Nat.zero_le _) h)] at h
  intro d hd; exact ne_of_lt (h d hd)

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