English
There exists a canonical ring homomorphism iterToSum from polynomials in S1 with coefficients in polynomials in S2 to polynomials in S1 ⊕ S2 with coefficients in R, realized by substituting X_inl and X_inr appropriately.
Русский
Существует естественное кольцевое однородное отображение iterToSum: MvPolynomial(S1, MvPolynomial(S2, R)) → MvPolynomial(S1 ⊕ S2, R), реализующее замену X_inl и X_inr на соответствующие индикаторы.
LaTeX
$$$\text{iterToSum} : MvPolynomial\,S_1\,(MvPolynomial\,S_2\,R) \to\+\* MvPolynomial\,(S_1\oplus S_2)\,R$$$
Lean4
/-- The function from multivariable polynomials in one type,
with coefficients in multivariable polynomials in another type,
to multivariable polynomials in the sum of the two types.
See `sumRingEquiv` for the ring isomorphism.
-/
def iterToSum : MvPolynomial S₁ (MvPolynomial S₂ R) →+* MvPolynomial (S₁ ⊕ S₂) R :=
eval₂Hom (eval₂Hom C (X ∘ Sum.inr)) (X ∘ Sum.inl)
