English
For S, τ, and x, with a ring hom f and a family g, the evaluation after eval₂ equals eval₂ with composed maps: eval₂ f g p = ... (precise statement as in lemma).
Русский
Для соответствующих структур и x выполняется равенство, связывающее eval₂ через композицию и map.
LaTeX
$$$$\operatorname{eval}_2 f g p = \operatorname{eval}_2 (\operatorname{eval}_x \circ f) (\lambda s. \operatorname{eval}_x(g(s))) p.$$$$
Lean4
theorem eval_eval₂ {S τ : Type*} {x : τ → S} [CommSemiring S] (f : R →+* MvPolynomial τ S) (g : σ → MvPolynomial τ S)
(p : MvPolynomial σ R) : eval x (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => eval x (g s)) p :=
by
apply induction_on p
· simp
· intro p q hp hq
simp [hp, hq]
· intro p n hp
simp [hp]
