rename_eq — Mathlib

English

Renaming a polynomial equals applying a double mapDomain: rename_f p = Finsupp.mapDomain (Finsupp.mapDomain f) p.

Русский

Переименование полинома эквивалентно применению двойного отображения mapDomain: rename_f p = Finsupp.mapDomain (Finsupp.mapDomain f) p.

LaTeX

$$$\\text{rename } f\\, p = \\mathrm{Finsupp.mapDomain}(\\mathrm{Finsupp.mapDomain} f)\\, p.$$$

Lean4

theorem rename_eq (f : σ → τ) (p : MvPolynomial σ R) : rename f p = Finsupp.mapDomain (Finsupp.mapDomain f) p := by
  simp_rw [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply, X_pow_eq_monomial, ←
    monomial_finsupp_sum_index, ← single_eq_monomial]

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