eval_intCast — Mathlib

English

Let R be a ring. For any integer n and any x ∈ R, the evaluation of the constant polynomial n at x equals n (viewed in R).

Русский

Пусть R — кольцо. Для любого целого n и любого x ∈ R значение константного полинома n при подстановке x равно n (в R).

LaTeX

$$$(n : R[X]).eval\\ x = n$$$

Lean4

@[simp]
theorem eval_intCast {n : ℤ} {x : R} : (n : R[X]).eval x = n := by simp only [← C_eq_intCast, eval_C]

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