evalEval_natCast

Mathlib.Algebra.Polynomial.Bivariate

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

English

For every n ∈ ℕ, the evaluation of the natural cast n in R[X][Y] at (x, y) equals n.

Русский

Пусть n ∈ ℕ. Значение отображения natCast в R[X][Y] при (x, y) равно n.

LaTeX

$$$ (n : R[X][Y]).evalEval\\ x\\ y = n $$$

Lean4

@[simp]
theorem evalEval_natCast (x y : R) (n : ℕ) : (n : R[X][Y]).evalEval x y = n := by simp only [evalEval, eval_natCast]

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

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

Разделы

Аффилиация

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