Scaling the variables of a homogeneous polynomial

Evaluating a homogeneous polynomial of degree n after multiplying every variable by a multiplies its value by a ^ n. This permits normalizing linear substitutions without expanding the polynomial.

The results live in MvPolynomial.IsHomogeneous, so a homogeneity proof supports dot notation such as hp.eval₂_const_mul, hp.aeval_smul, and hp.eval_smul.

The file also records MvPolynomial.isHomogeneous_coeff_prod_X_sub_C: the coefficients of a product of linear factors X - C Ψ with homogeneous Ψ of degree m are homogeneous.

theorem MvPolynomial.IsHomogeneous.eval₂_const_mul {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] {p : MvPolynomial σ R} {n : ℕ} (hp : p.IsHomogeneous n) (f : R →+* S) (g : σ → S) (a : S) : MvPolynomial.eval₂ f (fun (i : σ) => a * g i) p = a ^ n * MvPolynomial.eval₂ f g p

Scaling all variables by a scales the value of a degree-n homogeneous polynomial by a ^ n, after any change of coefficient ring.

This is not a global simp lemma: the degree n cannot be inferred from its left-hand side.

theorem MvPolynomial.IsHomogeneous.aeval_smul {σ : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} [CommSemiring R] [CommSemiring S] [CommSemiring A] [Algebra R A] [Algebra S A] {p : MvPolynomial σ R} {n : ℕ} (hp : p.IsHomogeneous n) (g : σ → A) (a : S) : (MvPolynomial.aeval (a • g)) p = a ^ n • (MvPolynomial.aeval g) p

Scaling the variables of a homogeneous polynomial by a scalar scales its algebra evaluation by the corresponding power of that scalar. The scalar algebra may differ from the coefficient algebra.

theorem MvPolynomial.IsHomogeneous.eval_smul {σ : Type u_1} {R : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {n : ℕ} (hp : p.IsHomogeneous n) (g : σ → R) (a : R) : (eval (a • g)) p = a ^ n • (eval g) p

Scaling the variables of a homogeneous polynomial scales its evaluation by the corresponding power of the scalar.

theorem MvPolynomial.isHomogeneous_coeff_prod_X_sub_C {σ : Type u_1} {R : Type u_2} [CommRing R] {ι : Type u_3} (s : Finset ι) (Ψ : ι → MvPolynomial σ R) {m : ℕ} (hΨ : ∀ i ∈ s, (Ψ i).IsHomogeneous m) (k : ℕ) : ((∏ i ∈ s, (Polynomial.X - Polynomial.C (Ψ i))).coeff k).IsHomogeneous (m * (s.card - k))

The coefficient of X ^ k in a product of linear factors X - C Ψ, whose constant terms Ψ are all homogeneous of degree m, is homogeneous of degree m * (s.card - k).