English
Let f be a ring homomorphism, and g, h a family of mv-polynomials. Evaluation commutes with bind₁ in the natural way: applying eval₂Hom after bind₁ equals evaluating each h(i) and then combining by eval₂Hom.
Русский
Пусть f — гомоморфизм, и g, h — семейство многочленов. Оценивание через eval₂Hom commute с bind₁ естественным образом: применение eval₂Hom после bind₁ эквивалентно оцениванию каждого h(i) и затем объединению через eval₂Hom.
LaTeX
$$$$ \mathrm{eval}_2\mathrm{Hom}\, f\, g\, (\mathrm{bind}_1\, h\, \varphi) = \mathrm{eval}_2\mathrm{Hom}\, f\, (\lambda i. \mathrm{eval}_2\mathrm{Hom}\, f\, g\, (h i))\, \varphi $$$$
Lean4
theorem eval₂Hom_bind₁ (f : R →+* S) (g : τ → S) (h : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
eval₂Hom f g (bind₁ h φ) = eval₂Hom f (fun i => eval₂Hom f g (h i)) φ := by rw [hom_bind₁, eval₂Hom_comp_C]
