weightedTotalDegree_rename_of_injective

English

If e is an injective map between index sets, then the weighted total degree of rename(e)(P) with weight w equals the weighted total degree of P with weight w ∘ e.

Русский

При вводимом замещении по инъекции e взвешенная полная степень сохраняется: deg_w(rename_e(P)) = deg_{w∘e}(P).

LaTeX

$$$\\operatorname{weightedTotalDegree}_w(\\rename_e P) = \\operatorname{weightedTotalDegree}_{w \\circ e} P$$$

Lean4

theorem weightedTotalDegree_rename_of_injective {σ τ : Type*} {e : σ → τ} {w : τ → ℕ} {P : MvPolynomial σ R}
    (he : Function.Injective e) : weightedTotalDegree w (rename e P) = weightedTotalDegree (w ∘ e) P := by
  classical
  unfold weightedTotalDegree
  rw [support_rename_of_injective he, Finset.sup_image]
  congr; ext; unfold weight; simp

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