coeff_sub — Mathlib

English

The coefficient of the difference p − q at index n equals the difference of the coefficients at n: coeff(p − q, n) = coeff(p, n) − coeff(q, n).

Русский

Коэффициент разности p − q на позиции n равен разности коэффициентов: coeff(p − q, n) = coeff(p, n) − coeff(q, n).

LaTeX

$$$\operatorname{coeff}(p - q, n) = \operatorname{coeff}(p, n) - \operatorname{coeff}(q, n)$$$

Lean4

@[simp]
theorem coeff_sub (p q : R[X]) (n : ℕ) : coeff (p - q) n = coeff p n - coeff q n :=
  by
  rcases p with ⟨⟩
  rcases q with ⟨⟩
  rw [← ofFinsupp_sub, coeff, coeff, coeff, Finsupp.sub_apply]

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