coeff_C_mul_X — Mathlib

English

Coefficient of C x times X is given by if n = 1 then x else 0: coeff (C x · X) n = if n = 1 then x else 0.

Русский

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

LaTeX

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

Lean4

theorem coeff_C_mul_X (x : R) (n : ℕ) : coeff (C x * X : R[X]) n = if n = 1 then x else 0 := by
  rw [← pow_one X, coeff_C_mul_X_pow]

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