English
There is a ring homomorphism that converts multivariable polynomials in a sum type S1 ⊕ S₂ to polynomials in S₁ with coefficients in mv-polynomials in S₂ over R.
Русский
Существует кольцо-гомоморфизм, переводящий MV-многочлены в сумму S1 ⊕ S₂ в многочлены в S₁ с коэффициентами MV-многочленов в S₂ над R.
LaTeX
$$$$ sumToIter : \\text{MvPolynomial} (S_1 \\oplus S_2) R \\to\\+* \\text{MvPolynomial} S_1 (\\text{MvPolynomial} S_2 R). $$$$
Lean4
/-- The function from multivariable polynomials in a sum of two types,
to multivariable polynomials in one of the types,
with coefficients in multivariable polynomials in the other type.
See `sumRingEquiv` for the ring isomorphism.
-/
def sumToIter : MvPolynomial (S₁ ⊕ S₂) R →+* MvPolynomial S₁ (MvPolynomial S₂ R) :=
eval₂Hom (C.comp C) fun bc => Sum.recOn bc X (C ∘ X)
