evalEval_X

Mathlib.Algebra.Polynomial.Bivariate

URI: https://scilib.ai/kg/mathlib#Polynomial.evalEval_X

English

Evaluating the indeterminate X at (x, y) yields y.

Русский

Значение переменной X при (x, y) равно y.

LaTeX

$$$ X.evalEval\\ x\\ y = y $$$

Lean4

@[simp]
theorem evalEval_X (x y : R) : X.evalEval x y = y := by rw [evalEval, eval_X, eval_C]

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

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

Разделы

Аффилиация

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