coeff_X_pow — Mathlib

English

The coefficient of X^k at n is 1 if n = k and 0 otherwise: coeff (X^k) n = 1 if n = k, else 0.

Русский

Коэффициент X^k при n равен 1, если n = k, и 0 иначе: coeff(X^k) n = 1 при n = k, иначе 0.

LaTeX

$$$\operatorname{coeff}(X^{k}) n = \begin{cases} 1, & n = k \\ 0, & n \neq k \end{cases}$$$

Lean4

@[simp]
theorem coeff_X_pow (k n : ℕ) : coeff (X ^ k : R[X]) n = if n = k then 1 else 0 := by
  simp only [one_mul, RingHom.map_one, ← coeff_C_mul_X_pow]

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