coeff_intCast_mul — Mathlib

English

For p in R[X] and integer a, the coefficient of (a : S[X]) · p equals a times the coefficient of p.

Русский

Для p в R[X] и целого a: коэффициент (a : S[X]) · p равен a умноженному на коэффициент p.

LaTeX

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

Lean4

@[simp]
theorem coeff_intCast_mul [Ring S] {p : S[X]} {a : ℤ} {k : ℕ} : coeff ((a : S[X]) * p) k = a * coeff p k :=
  coeff_C_mul _

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