expand_comp_bind₁ — Mathlib

English

Expanding after binding with f is the same as binding after expanding each f(i).

Русский

Расширение после связывания по f равно связыванию после расширения каждого f(i).

LaTeX

$$$$ \operatorname{expand}(p) \circ \operatorname{bind₁}(f) = \operatorname{bind₁}(i \mapsto \operatorname{expand}(p)(f(i))). $$$$

Lean4

theorem expand_comp_bind₁ (p : ℕ) (f : σ → MvPolynomial τ R) :
    (expand p).comp (bind₁ f) = bind₁ fun i ↦ expand p (f i) :=
  by
  apply algHom_ext
  intro i
  simp only [AlgHom.comp_apply, bind₁_X_right]

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