degreeOf_rename_of_injective — Mathlib

English

If f: σ → τ is injective, then renaming the variables in p by f preserves the degree for corresponding indices: deg_{f(i)}(rename_f(p)) = deg_i(p) for all i.

Русский

Если f: σ → τ инъективна, то переименование переменных в p по f сохраняет степени: deg_{f(i)}(rename_f(p)) = deg_i(p) для всех i.

LaTeX

$$$\operatorname{degree}_{f(i)}(\mathrm{rename}_f(p)) = \operatorname{degree}_i(p) \quad(\forall i)$$$

Lean4

theorem degreeOf_rename_of_injective {p : MvPolynomial σ R} {f : σ → τ} (h : Function.Injective f) (i : σ) :
    degreeOf (f i) (rename f p) = degreeOf i p := by
  classical simp only [degreeOf, degrees_rename_of_injective h, Multiset.count_map_eq_count' f p.degrees h]

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