aeval_bind₂ — Mathlib

English

With suitable algebra structure, aeval commutes with bind₂ in the stated way.

Русский

При наличии необходимой алгебраической структуры aeval commute с bind₂ в указанном виде.

LaTeX

$$$$ \mathrm{aeval}\, f\, (\mathrm{bind}_2\, g\, \varphi) = \mathrm{eval}_2\mathrm{Hom}\, ((\uparrow(\mathrm{aeval}\, f) : _ →ₐ[S] _ ) \circ g)\, f\, \varphi $$$$

Lean4

theorem aeval_bind₂ [Algebra S T] (f : σ → T) (g : R →+* MvPolynomial σ S) (φ : MvPolynomial σ R) :
    aeval f (bind₂ g φ) = eval₂Hom ((↑(aeval f : _ →ₐ[S] _) : _ →+* _).comp g) f φ :=
  eval₂Hom_bind₂ _ _ _ _

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