English
A key equivalence respects renaming and composition with pUnitAlgEquiv, yielding the same transformed polynomial after appropriate renaming.
Русский
Ключевое соответствие сохраняет переименование и композицию с pUnitAlgEquiv, приводя к тем же преобразованным полиномам после соответствующего переименования.
LaTeX
$$$((\mathrm{finSuccEquiv}\,R\,n)\bigl(\mathrm{rename}( (\mathrm{Equiv.optionCongr}\ e).trans(\mathrm{finSuccEquiv}\ n).symm)\ \phi\bigr)) = \mathrm{Polynomial.map}(\mathrm{rename}\,e).toRingHom(\mathrm{optionEquivLeft}\;R\;\sigma\;\phi)$$$
Lean4
theorem toMvPolynomial_injective (i : σ) : Function.Injective (toMvPolynomial (R := R) i) :=
by
simp only [toMvPolynomial_eq_rename_comp, AlgHom.coe_comp, AlgHom.coe_coe, EquivLike.injective_comp]
exact MvPolynomial.rename_injective (fun x ↦ i) fun _ _ _ ↦ rfl
