mathlib documentation

ring_theory.polynomial.homogeneous

Homogeneous polynomials

A multivariate polynomial φ is homogeneous of degree n if all monomials occuring in φ have degree n.

Main definitions/lemmas

def mv_polynomial.is_homogeneous {σ : Type u_1} {R : Type u_3} [comm_semiring R] :
mv_polynomial σ R → Prop

A multivariate polynomial φ is homogeneous of degree n if all monomials occuring in φ have degree n.

Equations
theorem mv_polynomial.is_homogeneous_monomial {σ : Type u_1} {R : Type u_3} [comm_semiring R] (d : σ →₀ ) (r : R) (n : ) :
∑ (i : σ) in d.support, d i = n(mv_polynomial.monomial d r).is_homogeneous n

theorem mv_polynomial.is_homogeneous_C (σ : Type u_1) {R : Type u_3} [comm_semiring R] (r : R) :

theorem mv_polynomial.is_homogeneous_zero (σ : Type u_1) (R : Type u_3) [comm_semiring R] (n : ) :

theorem mv_polynomial.is_homogeneous_one (σ : Type u_1) (R : Type u_3) [comm_semiring R] :

theorem mv_polynomial.is_homogeneous_X {σ : Type u_1} (R : Type u_3) [comm_semiring R] (i : σ) :

theorem mv_polynomial.is_homogeneous.coeff_eq_zero {σ : Type u_1} {R : Type u_3} [comm_semiring R] {φ : mv_polynomial σ R} {n : } (hφ : φ.is_homogeneous n) (d : σ →₀ ) :
∑ (i : σ) in d.support, d i nmv_polynomial.coeff d φ = 0

theorem mv_polynomial.is_homogeneous.inj_right {σ : Type u_1} {R : Type u_3} [comm_semiring R] {φ : mv_polynomial σ R} {m n : } :
φ.is_homogeneous mφ.is_homogeneous nφ 0m = n

theorem mv_polynomial.is_homogeneous.add {σ : Type u_1} {R : Type u_3} [comm_semiring R] {φ ψ : mv_polynomial σ R} {n : } :
φ.is_homogeneous nψ.is_homogeneous n+ ψ).is_homogeneous n

theorem mv_polynomial.is_homogeneous.sum {σ : Type u_1} {R : Type u_3} [comm_semiring R] {ι : Type u_2} (s : finset ι) (φ : ι → mv_polynomial σ R) (n : ) :
(∀ (i : ι), i s(φ i).is_homogeneous n)(∑ (i : ι) in s, φ i).is_homogeneous n

theorem mv_polynomial.is_homogeneous.mul {σ : Type u_1} {R : Type u_3} [comm_semiring R] {φ ψ : mv_polynomial σ R} {m n : } :
φ.is_homogeneous mψ.is_homogeneous n* ψ).is_homogeneous (m + n)

theorem mv_polynomial.is_homogeneous.prod {σ : Type u_1} {R : Type u_3} [comm_semiring R] {ι : Type u_2} (s : finset ι) (φ : ι → mv_polynomial σ R) (n : ι → ) :
(∀ (i : ι), i s(φ i).is_homogeneous (n i))(∏ (i : ι) in s, φ i).is_homogeneous (∑ (i : ι) in s, n i)

theorem mv_polynomial.is_homogeneous.total_degree {σ : Type u_1} {R : Type u_3} [comm_semiring R] {φ : mv_polynomial σ R} {n : } :
φ.is_homogeneous nφ 0φ.total_degree = n

def mv_polynomial.homogeneous_component {σ : Type u_1} {R : Type u_3} [comm_semiring R] :

homogeneous_component n φ is the part of φ that is homogeneous of degree n. See sum_homogeneous_component for the statement that φ is equal to the sum of all its homogeneous components.

Equations
theorem mv_polynomial.homogeneous_component_apply {σ : Type u_1} {R : Type u_3} [comm_semiring R] (n : ) (φ : mv_polynomial σ R) :
(mv_polynomial.homogeneous_component n) φ = ∑ (d : σ →₀ ) in finset.filter (λ (d : σ →₀ ), ∑ (i : σ) in d.support, d i = n) φ.support, mv_polynomial.monomial d (mv_polynomial.coeff d φ)

theorem mv_polynomial.homogeneous_component_eq_zero' {σ : Type u_1} {R : Type u_3} [comm_semiring R] (n : ) (φ : mv_polynomial σ R) :
(∀ (d : σ →₀ ), d φ.support∑ (i : σ) in d.support, d i n)(mv_polynomial.homogeneous_component n) φ = 0

theorem mv_polynomial.homogeneous_component_eq_zero {σ : Type u_1} {R : Type u_3} [comm_semiring R] (n : ) (φ : mv_polynomial σ R) :

theorem mv_polynomial.sum_homogeneous_component {σ : Type u_1} {R : Type u_3} [comm_semiring R] (φ : mv_polynomial σ R) :