totalDegree_renameEquiv — Mathlib

English

The total degree is invariant under renameEquiv, i.e., equals the original total degree.

Русский

Общая степень инвариантна относительно renameEquiv; она равна исходной.

LaTeX

$$$\\\\operatorname{totalDegree}(renameEquiv(R, f) p) = \\operatorname{totalDegree}(p)$$$

Lean4

theorem totalDegree_renameEquiv (f : σ ≃ τ) (p : MvPolynomial σ R) : (renameEquiv R f p).totalDegree = p.totalDegree :=
  (totalDegree_rename_le f p).antisymm (le_trans (by simp) (totalDegree_rename_le f.symm _))

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