Homogeneity in the coefficient variables, while retaining independent polynomial parameters. This property survives determinant expansion and extraction of any parameter coefficient.

def CCDN.CoefficientwiseHomogeneous {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] (f : MvPolynomial σ (MvPolynomial τ R)) (d : ℕ) : Prop

A polynomial f in the variables σ with coefficients in MvPolynomial τ R is coefficientwise homogeneous of degree d if each of its coefficients is a homogeneous polynomial of degree d in the variables τ.

Equations

• CCDN.CoefficientwiseHomogeneous f d = ∀ (m : σ →₀ ℕ), (f.coeff m).IsHomogeneous d

theorem CCDN.CoefficientwiseHomogeneous.zero {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] (d : ℕ) : CoefficientwiseHomogeneous 0 d

The zero polynomial is coefficientwise homogeneous of every degree.

theorem CCDN.CoefficientwiseHomogeneous.add {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] {f g : MvPolynomial σ (MvPolynomial τ R)} {d : ℕ} (hf : CoefficientwiseHomogeneous f d) (hg : CoefficientwiseHomogeneous g d) : CoefficientwiseHomogeneous (f + g) d

A sum of two coefficientwise homogeneous polynomials of degree d is coefficientwise homogeneous of degree d.

theorem CCDN.CoefficientwiseHomogeneous.neg {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] {f : MvPolynomial σ (MvPolynomial τ R)} {d : ℕ} (hf : CoefficientwiseHomogeneous f d) : CoefficientwiseHomogeneous (-f) d

The negation of a coefficientwise homogeneous polynomial of degree d is coefficientwise homogeneous of degree d.

theorem CCDN.CoefficientwiseHomogeneous.sum {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] {ι : Type u_4} (s : Finset ι) (f : ι → MvPolynomial σ (MvPolynomial τ R)) (d : ℕ) (hf : ∀ i ∈ s, CoefficientwiseHomogeneous (f i) d) : CoefficientwiseHomogeneous (∑ i ∈ s, f i) d

A finite sum of coefficientwise homogeneous polynomials of degree d is coefficientwise homogeneous of degree d.

theorem CCDN.CoefficientwiseHomogeneous.mul {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] {f g : MvPolynomial σ (MvPolynomial τ R)} {d e : ℕ} (hf : CoefficientwiseHomogeneous f d) (hg : CoefficientwiseHomogeneous g e) : CoefficientwiseHomogeneous (f * g) (d + e)

The product of coefficientwise homogeneous polynomials of degrees d and e is coefficientwise homogeneous of degree d + e.

theorem CCDN.CoefficientwiseHomogeneous.C_of_isHomogeneous {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] {f : MvPolynomial τ R} {d : ℕ} (hf : f.IsHomogeneous d) : CoefficientwiseHomogeneous (MvPolynomial.C f) d

The constant polynomial C f is coefficientwise homogeneous of degree d when f is a homogeneous polynomial of degree d in the variables τ.

theorem CCDN.CoefficientwiseHomogeneous.one {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] : CoefficientwiseHomogeneous 1 0

The polynomial 1 is coefficientwise homogeneous of degree 0.

theorem CCDN.CoefficientwiseHomogeneous.map_C {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] (f : MvPolynomial σ R) : CoefficientwiseHomogeneous ((MvPolynomial.map MvPolynomial.C) f) 0

A polynomial over R, with its coefficients viewed as constants of MvPolynomial τ R, is coefficientwise homogeneous of degree 0.

theorem CCDN.CoefficientwiseHomogeneous.prod {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] {ι : Type u_4} (s : Finset ι) (f : ι → MvPolynomial σ (MvPolynomial τ R)) (d : ι → ℕ) (hf : ∀ i ∈ s, CoefficientwiseHomogeneous (f i) (d i)) : CoefficientwiseHomogeneous (∏ i ∈ s, f i) (∑ i ∈ s, d i)

A finite product of coefficientwise homogeneous polynomials of degrees d i is coefficientwise homogeneous of degree ∑ i ∈ s, d i.

theorem CCDN.CoefficientwiseHomogeneous.det {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] {r : ℕ} (M : Matrix (Fin r) (Fin r) (MvPolynomial σ (MvPolynomial τ R))) (hM : ∀ (i j : Fin r), CoefficientwiseHomogeneous (M i j) 1) : CoefficientwiseHomogeneous M.det r

The determinant of an r × r matrix whose entries are coefficientwise homogeneous of degree 1 is coefficientwise homogeneous of degree r.