optionEquivLeft_X_none

Mathlib.Algebra.MvPolynomial.Equiv

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

English

Evaluating optionEquivLeft on the monomial X none gives the indeterminate X.

Русский

Применение optionEquivLeft к X none даёт переменную X.

LaTeX

$$$\text{optionEquivLeft} \;R\;S_1\; (X(\mathrm{none})) = X$$$

Lean4

theorem optionEquivLeft_X_none : optionEquivLeft R S₁ (X none) = Polynomial.X := by
  simp [optionEquivLeft_apply, aeval_X]

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

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

Разделы

Аффилиация

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