eval₂Hom_bind₂ — Mathlib

English

The full compatibility of eval₂Hom with bind₂ under composition.

Русский

Полная совместимость eval₂Hom с Bind₂ при композиции.

LaTeX

$$$$ \mathrm{eval}_2\mathrm{Hom}\, f\, g\, (\mathrm{bind}_2\, h\, \varphi) = \mathrm{eval}_2\mathrm{Hom}\, ((\mathrm{eval}_2\mathrm{Hom}\, f\, g) \circ h)\, g\, \varphi $$$$

Lean4

theorem eval₂Hom_bind₂ (f : S →+* T) (g : σ → T) (h : R →+* MvPolynomial σ S) (φ : MvPolynomial σ R) :
    eval₂Hom f g (bind₂ h φ) = eval₂Hom ((eval₂Hom f g).comp h) g φ :=
  RingHom.congr_fun (eval₂Hom_comp_bind₂ f g h) φ

Похожие утверждения