bind₂_map — Mathlib

English

Let f and g be ring homomorphisms as above and φ ∈ MvPolynomial σ R. Then performing map on φ and then bind₂ with f equals performing bind₂ with the composed map on φ.

Русский

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

LaTeX

$$$$ \mathrm{bind}_2\, f\, (\mathrm{map}\, g\, \varphi) = \mathrm{bind}_2\, ((\mathrm{map}\, g) \circ f)\, \varphi $$$$

Lean4

theorem bind₂_map (f : S →+* MvPolynomial σ T) (g : R →+* S) (φ : MvPolynomial σ R) :
    bind₂ f (map g φ) = bind₂ (f.comp g) φ := by simp [bind₂]

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