coeff_eq_zero — Mathlib

English

Let φ be homogeneous of degree n. Then for every multi-index d with degree(d) ≠ n, the coefficient of φ at d is zero.

Русский

Пусть φ однороден степени n. Тогда для любого многородного индекса d с deg(d) ≠ n коэффициент φ при d равен нулю.

LaTeX

$$$IsHomogeneous(\\phi, n) \\Rightarrow (\\forall d : \\sigma \\to{\\mathbb N}, deg(d) \\neq n \\Rightarrow coeff(d, \\phi) = 0)$$$

Lean4

theorem coeff_eq_zero (hφ : IsHomogeneous φ n) {d : σ →₀ ℕ} (hd : d.degree ≠ n) : coeff d φ = 0 :=
  by
  rw [degree_eq_weight_one] at hd
  exact IsWeightedHomogeneous.coeff_eq_zero hφ d hd

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