coeff_natCast_mul — Mathlib

English

For a natural a with at least two, the coefficient of (ofNat(a) : R[X]) · p equals ofNat(a) times the coefficient of p.

Русский

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

LaTeX

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

Lean4

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

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