coeff_X_pow_mul' — Mathlib

English

For p ∈ R[X] and n, d ∈ ℕ, the coefficient of (X^n · p) at d equals coeff(p, d − n) if n ≤ d, and 0 otherwise.

Русский

Для p ∈ R[X] и n, d ∈ ℕ, коэффициент (X^n · p) при степени d равен coeff(p, d − n), если n ≤ d, иначе 0.

LaTeX

$$$$\operatorname{coeff}(X^n p, d) = \begin{cases} \operatorname{coeff}(p, d-n), & n \le d, \\ 0, & n > d. \end{cases}$$$$

Lean4

theorem coeff_X_pow_mul' (p : R[X]) (n d : ℕ) : (X ^ n * p).coeff d = ite (n ≤ d) (p.coeff (d - n)) 0 := by
  rw [(commute_X_pow p n).eq, coeff_mul_X_pow']

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