coeff_C_mul_X_pow — Mathlib

English

The coefficient of C x multiplied by X^k is x at position k and 0 elsewhere: coeff (C x · X^k) n = if n = k then x else 0.

Русский

Коэффициент при умножении C x на X^k равен x при позиции k и 0 иначе: coeff(C x · X^k) n = if n = k then x else 0.

LaTeX

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

Lean4

theorem coeff_C_mul_X_pow (x : R) (k n : ℕ) : coeff (C x * X ^ k : R[X]) n = if n = k then x else 0 :=
  by
  rw [C_mul_X_pow_eq_monomial, coeff_monomial]
  simp [eq_comm]

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