coeff_monomial_zero_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem coeff_monomial_zero_mul (p : R[X]) (d : ℕ) (r : R) : coeff (monomial 0 r * p) d = r * coeff p d :=
  coeff_monomial_mul p 0 d r

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