Euler's homogeneous identity

Main results

• IsHomogeneous.sum_X_mul_pderiv: Euler's identity for homogeneous polynomials: for a multivariate homogeneous polynomial, the product of each variable with the derivative with respect to that variable sums up to the degree times the polynomial.
• IsWeightedHomogeneous.sum_weight_X_mul_pderiv: the weighted version of Euler's identity.

theorem MvPolynomial.IsWeightedHomogeneous.pderiv {R : Type u_1} {σ : Type u_2} {M : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} [AddCancelCommMonoid M] {w : σ → M} {n n' : M} {i : σ} (h : IsWeightedHomogeneous w φ n) (h' : n' + w i = n) : IsWeightedHomogeneous w ((pderiv i) φ) n'

theorem MvPolynomial.IsHomogeneous.pderiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ} {i : σ} (h : φ.IsHomogeneous n) : ((pderiv i) φ).IsHomogeneous (n - 1)

theorem MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} [Fintype σ] {n : ℕ} {w : σ → ℕ} (h : IsWeightedHomogeneous w φ n) : ∑ i : σ, w i • (X i * (pderiv i) φ) = n • φ

Euler's identity for weighted homogeneous polynomials.

theorem MvPolynomial.IsHomogeneous.sum_X_mul_pderiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} [Fintype σ] {n : ℕ} (h : φ.IsHomogeneous n) : ∑ i : σ, X i * (pderiv i) φ = n • φ

Euler's identity for homogeneous polynomials.