coeff_mul_monomial — Mathlib

English

For p ∈ R[X], n ∈ ℕ and r ∈ R, the coefficient of ((monomial n r) · p) at d+n equals r · coeff(p, d).

Русский

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

LaTeX

$$$$\operatorname{coeff}( (\text{monomial } n\; r) \cdot p, d+n) = r \cdot \operatorname{coeff}(p, d)$$$$

Lean4

theorem coeff_mul_monomial (p : R[X]) (n d : ℕ) (r : R) : coeff (p * monomial n r) (d + n) = coeff p d * r := by
  rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]

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