Coefficients_aeval_mem_lSpace_of_isHomogeneous.lean

theorem mul_coefficients_mem_lSpace
    {K F τ : Type*} [Field K] [Field F] [Algebra K F]
    {D E : Divisor K F} {p q : MvPolynomial τ F}
    (hp : p ∈ MvPolynomial.coeffsIn τ (LSpace D))
    (hq : q ∈ MvPolynomial.coeffsIn τ (LSpace E)) :
    p * q ∈ MvPolynomial.coeffsIn τ (LSpace (D + E))

theorem pow_coefficients_mem_lSpace
    {K F τ : Type*} [Field K] [Field F] [Algebra K F]
    {D : Divisor K F} {p : MvPolynomial τ F}
    (hp : p ∈ MvPolynomial.coeffsIn τ (LSpace D)) (n : ℕ) :
    p ^ n ∈ MvPolynomial.coeffsIn τ (LSpace (n • D))

theorem coefficients_aeval_mem_lSpace_of_isHomogeneous
    {K F σ τ : Type*} [Field K] [Field F] [Algebra K F]
    {d : ℕ} (p : MvPolynomial σ F) (q : σ → MvPolynomial τ F)
    (D E : Divisor K F) (hhom : p.IsHomogeneous d)
    (hp : ∀ a : σ →₀ ℕ, p.coeff a ∈ LSpace E)
    (hq : ∀ i : σ, ∀ a : τ →₀ ℕ, (q i).coeff a ∈ LSpace D) :
    ∀ a : τ →₀ ℕ, (MvPolynomial.aeval q p).coeff a ∈ LSpace (E + d • D)