coeff_C_mul — Mathlib

English

The coefficient of C a times p equals a times the coefficient of p: coeff (C a · p) n = a · coeff p n.

Русский

Коэффициент множителя C a на полином p равен a умноженному на коэффициент p: coeff(C a · p) n = a · coeff p n.

LaTeX

$$$\operatorname{coeff}(C a \cdot p) n = a \cdot \operatorname{coeff}(p, n)$$$

Lean4

@[simp]
theorem coeff_C_mul (p : R[X]) : coeff (C a * p) n = a * coeff p n :=
  by
  rcases p with ⟨p⟩
  simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]
  exact AddMonoidAlgebra.single_zero_mul_apply p a n

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