English
If p is a polynomial on Fin(N+1) with homogeneous image under a certain equivalence, then its coeff_i is homogeneous of degree j whenever i+j=n.
Русский
Если p — полином на Fin(N+1) и имеет однородность в образе под указанной эквив., то коэффициент при i однороден степени j при i+j=n.
LaTeX
$$For [Finite σ], if (optionEquivLeft R σ).symm p IsHomogeneous n, then ∀ i j, i + j = n → (p.coeff i).IsHomogeneous j$$
Lean4
theorem finSuccEquiv_coeff_isHomogeneous {N : ℕ} {φ : MvPolynomial (Fin (N + 1)) R} {n : ℕ} (hφ : φ.IsHomogeneous n)
(i j : ℕ) (h : i + j = n) : ((finSuccEquiv _ _ φ).coeff i).IsHomogeneous j :=
by
intro d hd
rw [finSuccEquiv_coeff_coeff] at hd
have h' : (weight 1) (Finsupp.cons i d) = i + j := by
simpa [Finset.sum_subset_zero_on_sdiff (g := d.cons i) (d.cons_support (y := i)) (by simp) (fun _ _ ↦ rfl),
← h] using hφ hd
simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum_cons, add_right_inj] at h' ⊢
exact h'
