coeff_X_pow_self — Mathlib

English

Let R be a semiring and X the indeterminate in the polynomial ring R[X]. Then for every natural number n, the coefficient of X^n in X^n is 1.

Русский

Пусть R — полупсеприруемое кольцо, а X — переменная в кольце многочленов R[X]. Тогда при любом натуральном n коэффициент при X^n в X^n равен 1.

LaTeX

$$$$\operatorname{coeff}(X^n : R[X]) n = 1$$$$

Lean4

theorem coeff_X_pow_self (n : ℕ) : coeff (X ^ n : R[X]) n = 1 := by simp

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