join₂_comp_map

Mathlib.Algebra.MvPolynomial.Monad

URI: https://scilib.ai/kg/mathlib#MvPolynomial.join₂_comp_map

English

The composition of join₂ with map f equals bind₂ f.

Русский

Составление join₂ с map f равно bind₂ f.

LaTeX

$$$\text{join}_2 \circ (\text{map } f) = \text{bind}_2 f$$$

Lean4

@[simp]
theorem join₂_comp_map (f : R →+* MvPolynomial σ S) : join₂.comp (map f) = bind₂ f :=
  RingHom.ext <| join₂_map _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru