toMvPolynomial_eq_rename_comp — Mathlib

English

The map sending i to the corresponding univariate polynomial coincides with renaming after an appropriate unit-equivalence.

Русский

Отображение toMvPolynomial и переименование согласованы через подходящую единичную эквивалентность.

LaTeX

$$$\text{toMvPolynomial}(i) = (\mathrm{rename}((\mathrm{Equiv.optionCongr}\ e).trans(\mathrm{finSuccEquiv}\ n).symm)).comp(\mathrm{pUnitAlgEquiv}\;R)^{-1}$$$

Lean4

theorem toMvPolynomial_eq_rename_comp (i : σ) :
    toMvPolynomial (R := R) i = (MvPolynomial.rename (fun _ : Unit ↦ i)).comp (MvPolynomial.pUnitAlgEquiv R).symm :=
  by
  ext
  simp

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