bind₂_C_right

Mathlib.Algebra.MvPolynomial.Monad

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

English

For any r ∈ R, bind₂ f (C r) = f r; constants are substituted by f.

Русский

Для любого r ∈ R, bind₂ f (C r) = f r; константы подставляются через f.

LaTeX

$$$\text{bind}_2 f (C r) = f r$$$

Lean4

@[simp]
theorem bind₂_C_right (f : R →+* MvPolynomial σ S) (r : R) : bind₂ f (C r) = f r :=
  eval₂Hom_C f X r

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

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

Разделы

Аффилиация

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