# mathlib3documentation

ring_theory.mv_polynomial.homogeneous

# Homogeneous polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions/lemmas #

• is_homogeneous φ n: a predicate that asserts that φ is homogeneous of degree n.
• homogeneous_submodule σ R n: the submodule of homogeneous polynomials of degree n.
• homogeneous_component n: the additive morphism that projects polynomials onto their summand that is homogeneous of degree n.
• sum_homogeneous_component: every polynomial is the sum of its homogeneous components
def mv_polynomial.is_homogeneous {σ : Type u_1} {R : Type u_3} (φ : R) (n : ) :
Prop

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

Equations
def mv_polynomial.homogeneous_submodule (σ : Type u_1) (R : Type u_3) (n : ) :
R)

The submodule of homogeneous mv_polynomials of degree n.

Equations
Instances for mv_polynomial.homogeneous_submodule
@[simp]
theorem mv_polynomial.mem_homogeneous_submodule {σ : Type u_1} {R : Type u_3} (n : ) (p : R) :
theorem mv_polynomial.homogeneous_submodule_eq_finsupp_supported (σ : Type u_1) (R : Type u_3) (n : ) :
= {d : σ →₀ | d.support.sum (λ (i : σ), d i) = n}

While equal, the former has a convenient definitional reduction.

theorem mv_polynomial.homogeneous_submodule_mul {σ : Type u_1} {R : Type u_3} (m n : ) :
theorem mv_polynomial.is_homogeneous_monomial {σ : Type u_1} {R : Type u_3} (d : σ →₀ ) (r : R) (n : ) (hn : d.support.sum (λ (i : σ), d i) = n) :
n
theorem mv_polynomial.is_homogeneous_of_total_degree_zero (σ : Type u_1) {R : Type u_3} {p : R} (hp : p.total_degree = 0) :
theorem mv_polynomial.is_homogeneous_C (σ : Type u_1) {R : Type u_3} (r : R) :
theorem mv_polynomial.is_homogeneous_zero (σ : Type u_1) (R : Type u_3) (n : ) :
theorem mv_polynomial.is_homogeneous_one (σ : Type u_1) (R : Type u_3)  :
theorem mv_polynomial.is_homogeneous_X {σ : Type u_1} (R : Type u_3) (i : σ) :
theorem mv_polynomial.is_homogeneous.coeff_eq_zero {σ : Type u_1} {R : Type u_3} {φ : R} {n : } (hφ : φ.is_homogeneous n) (d : σ →₀ ) (hd : d.support.sum (λ (i : σ), d i) n) :
= 0
theorem mv_polynomial.is_homogeneous.inj_right {σ : Type u_1} {R : Type u_3} {φ : R} {m n : } (hm : φ.is_homogeneous m) (hn : φ.is_homogeneous n) (hφ : φ 0) :
m = n
theorem mv_polynomial.is_homogeneous.add {σ : Type u_1} {R : Type u_3} {φ ψ : R} {n : } (hφ : φ.is_homogeneous n) (hψ : ψ.is_homogeneous n) :
+ ψ).is_homogeneous n
theorem mv_polynomial.is_homogeneous.sum {σ : Type u_1} {R : Type u_3} {ι : Type u_2} (s : finset ι) (φ : ι ) (n : ) (h : (i : ι), i s (φ i).is_homogeneous n) :
(s.sum (λ (i : ι), φ i)).is_homogeneous n
theorem mv_polynomial.is_homogeneous.mul {σ : Type u_1} {R : Type u_3} {φ ψ : R} {m n : } (hφ : φ.is_homogeneous m) (hψ : ψ.is_homogeneous n) :
* ψ).is_homogeneous (m + n)
theorem mv_polynomial.is_homogeneous.prod {σ : Type u_1} {R : Type u_3} {ι : Type u_2} (s : finset ι) (φ : ι ) (n : ι ) (h : (i : ι), i s (φ i).is_homogeneous (n i)) :
(s.prod (λ (i : ι), φ i)).is_homogeneous (s.sum (λ (i : ι), n i))
theorem mv_polynomial.is_homogeneous.total_degree {σ : Type u_1} {R : Type u_3} {φ : R} {n : } (hφ : φ.is_homogeneous n) (h : φ 0) :
@[protected, instance]

The homogeneous submodules form a graded ring. This instance is used by direct_sum.comm_semiring and direct_sum.algebra.

noncomputable def mv_polynomial.homogeneous_component {σ : Type u_1} {R : Type u_3} (n : ) :

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.coeff_homogeneous_component {σ : Type u_1} {R : Type u_3} (n : ) (φ : R) (d : σ →₀ ) :
= ite (d.support.sum (λ (i : σ), d i) = n) φ) 0
theorem mv_polynomial.homogeneous_component_apply {σ : Type u_1} {R : Type u_3} (n : ) (φ : R) :
= (finset.filter (λ (d : σ →₀ ), d.support.sum (λ (i : σ), d i) = n) φ.support).sum (λ (d : σ →₀ ), φ))
theorem mv_polynomial.homogeneous_component_is_homogeneous {σ : Type u_1} {R : Type u_3} (n : ) (φ : R) :
@[simp]
theorem mv_polynomial.homogeneous_component_zero {σ : Type u_1} {R : Type u_3} (φ : R) :
@[simp]
theorem mv_polynomial.homogeneous_component_C_mul {σ : Type u_1} {R : Type u_3} (φ : R) (n : ) (r : R) :
theorem mv_polynomial.homogeneous_component_eq_zero' {σ : Type u_1} {R : Type u_3} (n : ) (φ : R) (h : (d : σ →₀ ), d φ.support d.support.sum (λ (i : σ), d i) n) :
theorem mv_polynomial.homogeneous_component_eq_zero {σ : Type u_1} {R : Type u_3} (n : ) (φ : R) (h : φ.total_degree < n) :
theorem mv_polynomial.sum_homogeneous_component {σ : Type u_1} {R : Type u_3} (φ : R) :
(finset.range (φ.total_degree + 1)).sum (λ (i : ), = φ
theorem mv_polynomial.homogeneous_component_homogeneous_polynomial {σ : Type u_1} {R : Type u_3} (m n : ) (p : R) (h : p ) :
= ite (m = n) p 0