English
Expanding a polynomial along a sum of two index sets corresponds to splitting the evaluation accordingly, i.e., evaluating with Sum.elim equals iterated evaluation with X and C composed appropriately.
Русский
Расширение полинома по сумме двух индексов эквивалентно разбиению оценки по частям, используя Sum.elim.
LaTeX
$$$$ \operatorname{aeval}(\operatorname{Sum.elim} g (\mathrm{algebraMap}(S,T) \circ f)) p = \operatorname{aeval}(g)(\operatorname{aeval}(\operatorname{Sum.elim} X (C \circ f)) p). $$$$
Lean4
theorem aeval_sumElim {σ τ : Type*} (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (g : σ → T) :
(aeval (Sum.elim g (algebraMap S T ∘ f))) p = (aeval g) ((aeval (Sum.elim X (C ∘ f))) p) := by
induction p using MvPolynomial.induction_on with
| C r => simp [← IsScalarTower.algebraMap_apply]
| add p q hp hq => simp [hp, hq]
| mul_X p i h => cases i <;> simp [h]
