coeff_mul_C — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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