coeff_mul_intCast — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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