aeval_bind₁ — Mathlib

English

Let f be an algebra hom and g a family of mv-polynomials. Then the algebra evaluation aeval f distributes over bind₁ in the expected way.

Русский

Пусть f — алгебра-гомоморфизм, а g — семейство mv-полиномов. Тогда алгебраическое вычисление aeval f распределяется через bind₁ как и ожидалось.

LaTeX

$$$$ \mathrm{aeval}\, f\; (\mathrm{bind}_1\, g\; \varphi) = \mathrm{aeval}\; (\lambda i. \mathrm{aeval}\, f\; (g i))\; \varphi $$$$

Lean4

theorem aeval_bind₁ [Algebra R S] (f : τ → S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
    aeval f (bind₁ g φ) = aeval (fun i => aeval f (g i)) φ :=
  eval₂Hom_bind₁ _ _ _ _

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