coeff_C_mul_X_pow — Mathlib

English

The coefficient of Cx multiplied by X^k at degree n is x if n = k, otherwise 0.

Русский

Коэффициент при n в произведении Cx·X^k равен x, если n = k, иначе 0.

LaTeX

$$$\\forall R\\ [\\operatorname{Semiring} R]\\, (x \\in R)\\, (k,n \\in \\mathbb{N}),\\ \\operatorname{coeff}_n( C x \\cdot X^k ) = \\begin{cases} x, & n = k \\\\ 0, & \\text{иначе} \\end{cases}$$$

Lean4

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

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