coeff_monomial_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem coeff_monomial_mul (p : R[X]) (n d : ℕ) (r : R) : coeff (monomial n r * p) (d + n) = r * coeff p d := by
  rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]
    -- This can already be proved by `simp`.

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