bind₁_rename — Mathlib

English

Let f and g be as above and φ ∈ MvPolynomial σ R. Then applying bind₁ after rename g equals applying bind₁ with the composed map to φ.

Русский

Пусть f и g как выше, и φ ∈ MvPolynomial σ R. Тогда применение bind₁ после переименования g эквивалентно применению bind₁ с композицией на φ.

LaTeX

$$$$ \mathrm{bind}_1\, f\, (\mathrm{rename}\, g\, \phi) = \mathrm{bind}_1\, (f \circ g)\, \phi $$$$

Lean4

theorem bind₁_rename {υ : Type*} (f : τ → MvPolynomial υ R) (g : σ → τ) (φ : MvPolynomial σ R) :
    bind₁ f (rename g φ) = bind₁ (f ∘ g) φ :=
  AlgHom.congr_fun (bind₁_comp_rename f g) φ

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