coeff_add

Mathlib.Algebra.Polynomial.Coeff

URI: https://scilib.ai/kg/mathlib#Polynomial.coeff_add

← MathLib Explorer

English

The coefficient extraction is linear: coeff(p + q) n = coeff(p,n) + coeff(q,n).

Русский

Извлечение коэффициента линейно: coeff(p+q,n) = coeff(p,n) + coeff(q,n).

LaTeX

$$coeff(p + q,n) = coeff(p,n) + coeff(q,n)$$

Lean4

@[simp]
theorem coeff_add (p q : R[X]) (n : ℕ) : coeff (p + q) n = coeff p n + coeff q n :=
  by
  rcases p with ⟨⟩
  rcases q with ⟨⟩
  simp_rw [← ofFinsupp_add, coeff]
  exact Finsupp.add_apply _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru