degrees_rename_of_injective — Mathlib

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

Похожие утверждения