rename_toMvPolynomial — Mathlib

English

Renaming commutes with the embedding of univariate polynomials into multivariate polynomials.

Русский

Переименование коммутирует со встроением одновариантного полинома в многовариантный полином.

LaTeX

$$$\mathrm{rename}(f) \bigl( p^{\mathrm{toMvPolynomial}(a)} \bigr) = p^{\mathrm{toMvPolynomial}(f(a))}$$$

Lean4

@[simp]
theorem rename_toMvPolynomial (f : σ → τ) (a : σ) (p : R[X]) :
    (rename (R := R) f) (p.toMvPolynomial a) = p.toMvPolynomial (f a) :=
  DFunLike.congr_fun (rename_comp_toMvPolynomial ..) p

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