English
Evaluating with a second-level polynomial inside the evaluation gives the same as a single evaluation after composing with inner evaluation: eval₂ f (i ↦ eval₂ f g (q i)) p = eval₂ f g (eval₂ C q p).
Русский
Оценка с вложенным вторичным полиномом эквивалентна одиночной оценке после композиции: eval₂ f (i ↦ eval₂ f g (q i)) p = eval₂ f g (eval₂ C q p).
LaTeX
$$$\\mathrm{eval}_2 f \\bigl( \\lambda t. \\mathrm{eval}_2 f g (q(t)) \\bigr) p = \\mathrm{eval}_2 f g (\\mathrm{eval}_2 \\mathbf{C} q p)$$$
Lean4
theorem eval₂_assoc (q : S₂ → MvPolynomial σ R) (p : MvPolynomial S₂ R) :
eval₂ f (fun t => eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p) :=
by
change _ = eval₂Hom f g (eval₂ C q p)
rw [eval₂_comp_left (eval₂Hom f g)]; congr with a; simp
