intCast_coeff_zero — Mathlib

English

For any integer i and any ring R, the constant term of i considered as a polynomial in R[X] is i. In particular, the 0-th coefficient of (i : R[X]) equals i.

Русский

Для любого целого числа i и любого кольца R константный член полинома, полученного из i в R[X], равен i.

LaTeX

$$$ (i : R[X]).coeff 0 = i $$$

Lean4

@[simp]
theorem intCast_coeff_zero {i : ℤ} {R : Type*} [Ring R] : (i : R[X]).coeff 0 = i := by cases i <;> simp

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