English
Let f and g be ring homomorphisms as above, and φ ∈ MvPolynomial σ R. Then applying map to the result of bind₂ f φ is the same as performing bind₂ with the composed map on φ.
Русский
Пусть f и g — гомоморфизмы колец, и φ ∈ MvPolynomial σ R. Тогда применение map к результату bind₂ f φ эквивалентно выполнению bind₂ с композицией на φ.
LaTeX
$$$$ \mathrm{map}\, g\, (\mathrm{bind}_2\, f\, \varphi) = \mathrm{bind}_2\, ((\mathrm{map}\, g) \circ f)\, \varphi $$$$
Lean4
theorem map_bind₂ (f : R →+* MvPolynomial σ S) (g : S →+* T) (φ : MvPolynomial σ R) :
map g (bind₂ f φ) = bind₂ ((map g).comp f) φ :=
by
simp only [bind₂, eval₂_comp_right, coe_eval₂Hom, eval₂_map]
congr 1 with : 1
simp only [Function.comp_apply, map_X]
