bind₁_X_right

Mathlib.Algebra.MvPolynomial.Monad

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

English

For any i, bind₁ f (X_i) = f i.

Русский

Для любого i: bind₁ f (X_i) = f i.

LaTeX

$$$\text{bind}_1 f (X_i) = f i$$$

Lean4

@[simp]
theorem bind₁_X_right (f : σ → MvPolynomial τ R) (i : σ) : bind₁ f (X i) = f i :=
  aeval_X f i

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

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

Разделы

Аффилиация

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