bind₁_X_left

Mathlib.Algebra.MvPolynomial.Monad

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

English

The map on variables satisfies bind₁ (X) = default X, i.e., X is fixed under the X-map.

Русский

Картина отображения переменных удовлетворяет bind₁ (X) = X.

LaTeX

$$$\text{bind}_1 (X) = \mathrm{X}$$$

Lean4

@[simp]
theorem bind₁_X_left : bind₁ (X : σ → MvPolynomial σ R) = AlgHom.id R _ :=
  by
  ext1 i
  simp

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

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

Разделы

Аффилиация

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