Euler's homogeneous identity #
Main resutls #
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 : MvPolynomial.IsWeightedHomogeneous w φ n)
(h' : n' + w i = n)
:
MvPolynomial.IsWeightedHomogeneous w ((MvPolynomial.pderiv i) φ) n'
theorem
MvPolynomial.IsHomogeneous.pderiv
{R : Type u_1}
{σ : Type u_2}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
{i : σ}
(h : φ.IsHomogeneous n)
:
((MvPolynomial.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 : MvPolynomial.IsWeightedHomogeneous w φ n)
:
∑ i : σ, w i • (MvPolynomial.X i * (MvPolynomial.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 : σ, MvPolynomial.X i * (MvPolynomial.pderiv i) φ = n • φ
Euler's identity for homogeneous polynomials.