English
If f is injective, then degrees(rename f p) equals (degrees p).map f.
Русский
Если f инъективно, то degrees(rename f p) = (degrees p).map f.
LaTeX
$$$\text{Injective } f \Rightarrow \operatorname{degrees}(\operatorname{rename} f\; p) = (p.degrees).map f$$$
Lean4
theorem degrees_rename_of_injective {p : MvPolynomial σ R} {f : σ → τ} (h : Function.Injective f) :
degrees (rename f p) = (degrees p).map f := by
classical
simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h, support_rename_of_injective h,
Finset.sup_image]
refine Finset.sup_congr rfl fun x _ => ?_
exact (Finsupp.toMultiset_map _ _).symm