eval₂Hom_comp_bind₂ — Mathlib

English

Composition of eval₂Hom with bind₂ is compatible with composing h inside eval₂Hom.

Русский

Сложение eval₂Hom с bind₂ совместимо с введением композиции внутрь eval₂Hom.

LaTeX

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

Lean4

theorem eval₂Hom_comp_bind₂ (f : S →+* T) (g : σ → T) (h : R →+* MvPolynomial σ S) :
    (eval₂Hom f g).comp (bind₂ h) = eval₂Hom ((eval₂Hom f g).comp h) g := by ext : 2 <;> simp

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