coeff_mul_natCast — Mathlib

English

For any R, the coefficient of (a : R[X]) · p equals a times the coefficient of p, when a is a natural cast.

Русский

Для любого R коэффициент от (a : R[X]) · p равен a умножить на коэффициент p, когда a — натуральное приводимое число.

LaTeX

$$$\operatorname{coeff}((a : R[X]) \cdot p) k = a \cdot \operatorname{coeff}(p,k)$$$

Lean4

@[simp]
theorem coeff_mul_natCast {a k : ℕ} : coeff (p * (a : R[X])) k = coeff p k * (↑a : R) :=
  coeff_mul_C _ _ _

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