English
Renaming the variables by f: σ → τ yields degrees of rename(p) contained in degrees(p) mapped by f.
Русский
Переименование переменных по f: σ → τ дает, что степени rename(p) содержатся в degrees(p).map f.
LaTeX
$$$\operatorname{degrees}(\operatorname{rename} f\; p) ⊆ (p.degrees).map f$$$
Lean4
theorem degrees_rename (f : σ → τ) (φ : MvPolynomial σ R) : (rename f φ).degrees ⊆ φ.degrees.map f := by
classical
intro i
rw [mem_degrees, Multiset.mem_map]
rintro ⟨d, hd, hi⟩
obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
rw [sum_apply, Finsupp.sum] at hi
contrapose! hi
rw [Finset.sum_eq_zero]
intro j hj
simp only [mem_degrees] at hi
specialize hi j ⟨x, hx, hj⟩
rw [Finsupp.single_apply, if_neg hi]
