bind₂_comp_C

Mathlib.Algebra.MvPolynomial.Monad

URI: https://scilib.ai/kg/mathlib#MvPolynomial.bind₂_comp_C

English

As above, and also show that bind₂ with C commutes with join₂ in a certain way.

Русский

И дополнительно показать, что bind₂ с C коммутирует с join₂ в определенном месте.

LaTeX

$$$\text{bind}_2 (C) \text{ и } \text{join}_2$$$

Lean4

@[simp]
theorem bind₂_comp_C (f : R →+* MvPolynomial σ S) : (bind₂ f).comp C = f :=
  RingHom.ext <| bind₂_C_right _

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

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

Разделы

Аффилиация

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