rename_monomial — Mathlib

English

Renaming respects monomials: rename_f(monomial(d,r)) = monomial(d.mapDomain f, r).

Русский

Переименование сохраняет мономиалы: rename_f(monomial(d,r)) = monomial(d.mapDomain f, r).

LaTeX

$$$\\text{rename } f\\,\\bigl(\\mathrm{monomial}(d,r)\\bigr) = \\mathrm{monomial}(d\\,\\mathrm{mapDomain} f, r).$$$

Lean4

theorem rename_monomial (f : σ → τ) (d : σ →₀ ℕ) (r : R) : rename f (monomial d r) = monomial (d.mapDomain f) r :=
  by
  rw [rename, aeval_monomial, monomial_eq (s := Finsupp.mapDomain f d), Finsupp.prod_mapDomain_index, algebraMap_eq]
  · simp_rw [Function.comp_apply]
  · exact fun n => pow_zero _
  · exact fun n i₁ i₂ => pow_add _ _ _

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