expand_bind₁ — Mathlib

English

Expanding after bind₁ equals binding after mapping expansion to each argument.

Русский

Расширение после bind₁ равно связыванию после отображения расширения к каждому аргументу.

LaTeX

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

Lean4

theorem expand_bind₁ (p : ℕ) (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
    expand p (bind₁ f φ) = bind₁ (fun i ↦ expand p (f i)) φ := by rw [← AlgHom.comp_apply, expand_comp_bind₁]

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