totalDegree_rename_le — Mathlib

English

Under a variable renaming via an equivalence, the total degree remains unchanged.

Русский

При переименовании переменных через эквивалентность общая степень сохраняется.

LaTeX

$$$\\\\forall R σ τ (f : σ \\\\to τ) (p : MvPolynomial σ R), \\\\ operatorname{totalDegree}(renameEquiv R f p) = totalDegree(p)$$$

Lean4

theorem totalDegree_rename_le (f : σ → τ) (p : MvPolynomial σ R) : (rename f p).totalDegree ≤ p.totalDegree :=
  Finset.sup_le fun b => by
    classical
    intro h
    rw [rename_eq] at h
    have h' := Finsupp.mapDomain_support h
    rw [Finset.mem_image] at h'
    rcases h' with ⟨s, hs, rfl⟩
    exact (sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)

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