pderiv — Mathlib

English

Euler's identity for weighted homogeneous polynomials: the sum of w(i) X(i) pderiv i φ equals n φ.

Русский

Идентичность Эйлера для взвешенно однородных полиномов: сумма w(i) X(i) pderiv i φ равна n φ.

LaTeX

$$$\\sum_{i \\in \\sigma} w(i) \\cdot (X(i) \\cdot pderiv\\,i\\, \\phi) = n \\cdot \\phi$$$

Lean4

protected theorem pderiv {n : ℕ} {i : σ} (h : φ.IsHomogeneous n) : (pderiv i φ).IsHomogeneous (n - 1) :=
  by
  obtain _ | n := n
  · rw [← totalDegree_zero_iff_isHomogeneous, totalDegree_eq_zero_iff_eq_C] at h
    rw [h, pderiv_C]; apply isHomogeneous_zero
  · exact IsWeightedHomogeneous.pderiv h rfl

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