optionEquivLeft_X_some

Mathlib.Algebra.MvPolynomial.Equiv

URI: https://scilib.ai/kg/mathlib#MvPolynomial.optionEquivLeft_X_some

English

Evaluating optionEquivLeft on the monomial X (some x) yields the constant polynomial C(X x).

Русский

Применение optionEquivLeft к мономиалу X(some x) даёт константный полином C(X x).

LaTeX

$$$\text{optionEquivLeft} \;R\;S_1\; (X(\mathrm{some}\, x)) = C(X x)$$$

Lean4

theorem optionEquivLeft_X_some (x : S₁) : optionEquivLeft R S₁ (X (some x)) = Polynomial.C (X x) := by
  simp [optionEquivLeft_apply, aeval_X]

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

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

Разделы

Аффилиация

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