rename_comp_toMvPolynomial — Mathlib

English

Repeated instance of the compatibility between renaming and aeval in the polynomial context.

Русский

Повторное утверждение совместимости переименования и aeval в контексте полиномов.

LaTeX

$$$\mathrm{rename}\;f\bigl(\mathrm{Polynomial.aeval} (X_i)\, p\bigr) = \mathrm{Polynomial.aeval} (X_{f(i)})\, p$$$

Lean4

@[simp]
theorem rename_comp_toMvPolynomial (f : σ → τ) (a : σ) :
    (rename (R := R) f).comp (Polynomial.toMvPolynomial a) = Polynomial.toMvPolynomial (f a) :=
  by
  ext
  simp

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