English
For a finite polynomial under the finite successor equivalence, the i-th coefficient is homogeneous of a degree determined by i and the total degree n.
Русский
При применении эквивалентности финитного следования коэффициент i монома сохраняет однородность степени, зависящей от i и суммарной степени n.
LaTeX
$$finSuccEquiv(φ) IsHomogeneous n → ∀ i j, i + j = n → ((finSuccEquiv φ).coeff i).IsHomogeneous j$$
Lean4
theorem eval₂ (hφ : φ.IsHomogeneous m) (f : R →+* MvPolynomial τ S) (g : σ → MvPolynomial τ S)
(hf : ∀ r, (f r).IsHomogeneous 0) (hg : ∀ i, (g i).IsHomogeneous n) : (eval₂ f g φ).IsHomogeneous (n * m) :=
by
apply IsHomogeneous.sum
intro i hi
rw [← zero_add (n * m)]
apply IsHomogeneous.mul (hf _) _
convert IsHomogeneous.prod _ _ (fun k ↦ n * i k) _
· rw [Finsupp.mem_support_iff] at hi
rw [← Finset.mul_sum, ← hφ hi, weight_apply]
simp_rw [smul_eq_mul, Finsupp.sum, Pi.one_apply, mul_one]
· rintro k -
apply (hg k).pow
