coeff_sub_eq_neg_right_of_lt

Mathlib.Algebra.Polynomial.Degree.Lemmas

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

← MathLib Explorer

English

If p.natDegree < n, then (p − q).coeff n = − q.coeff n.

Русский

Если p.natDegree < n, то (p − q).coeff n = − q.coeff n.

LaTeX

$$$(p - q).\coeff(n) = - q.\coeff(n)$ при $\operatorname{natDegree}(p) < n$$$

Lean4

theorem coeff_sub_eq_neg_right_of_lt (df : p.natDegree < n) : (p - q).coeff n = -q.coeff n := by
  rwa [sub_eq_add_neg, coeff_add_eq_right_of_lt, coeff_neg]

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

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

Разделы

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

Аффилиация

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