sum_X_mul_pderiv — Mathlib

English

Euler's identity for homogeneous polynomials: the sum of X_i pderiv i φ equals the total degree n times φ.

Русский

Идентичность Эйлера для однородных полиномов: сумма X_i pderiv_i φ равна n φ.

LaTeX

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

Lean4

/-- Euler's identity for homogeneous polynomials. -/
theorem sum_X_mul_pderiv (h : φ.IsHomogeneous n) : ∑ i : σ, X i * pderiv i φ = n • φ := by
  simp_rw [← h.sum_weight_X_mul_pderiv, Pi.one_apply, one_smul]

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