bind₁_C_right

Mathlib.Algebra.MvPolynomial.Monad

URI: https://scilib.ai/kg/mathlib#MvPolynomial.bind₁_C_right

English

For any x, bind₁ f (C x) = C x; constants are preserved under bind₁.

Русский

Для любого x константа C x сохраняется под действием bind₁.

LaTeX

$$$\text{bind}_1 f (C x) = C x$$$

Lean4

theorem bind₁_C_right (f : σ → MvPolynomial τ R) (x) : bind₁ f (C x) = C x :=
  algHom_C _ _

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

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

Разделы

Аффилиация

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