coeff_ofNat_mul — Mathlib

English

For a natural a, coeff (p · ofNat(a)) k = coeff p k · ofNat(a).

Русский

Для натурального a: коэффициент (p · ofNat(a)) k = коэффициент p k · ofNat(a).

LaTeX

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

Lean4

@[simp]
theorem coeff_ofNat_mul {a k : ℕ} [Nat.AtLeastTwo a] : coeff ((ofNat(a) : R[X]) * p) k = ofNat(a) * coeff p k :=
  coeff_C_mul _

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