English
The mvPolynomialEquivMvPolynomial construction provides a canonical ring equivalence between mv-polynomials of two different index sets using given f,g with compatibility on C and X.
Русский
Конструкция mvPolynomialEquivMvPolynomial задаёт каноническое кольцовое эквивалентство mv-многочленов двух наборов индексов через данные f,g совместимые на C и X.
LaTeX
$$$\text{mvPolynomialEquivMvPolynomial} \;R\;S_1\;S_2\;S_3\;f\;g\;h_{C}\;h_{X}\;h_{C'}; \text{сложная эквивалентность}$$$
Lean4
/-- The algebra isomorphism between multivariable polynomials in `Option S₁` and
polynomials with coefficients in `MvPolynomial S₁ R`.
-/
@[simps! -isSimp]
def optionEquivLeft : MvPolynomial (Option S₁) R ≃ₐ[R] Polynomial (MvPolynomial S₁ R) :=
AlgEquiv.ofAlgHom (MvPolynomial.aeval fun o => o.elim Polynomial.X fun s => Polynomial.C (X s))
(Polynomial.aevalTower (MvPolynomial.rename some) (X none)) (by ext : 2 <;> simp) (by ext i : 2; cases i <;> simp)
