nextCoeff_of_natDegree_pos

Mathlib.Algebra.Polynomial.Degree.Definitions

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

← MathLib Explorer

English

If 0 < natDegree(p), then nextCoeff(p) = coeff(p, natDegree(p) − 1).

Русский

Если 0 < natDegree(p), то nextCoeff(p) = coeff(p, natDegree(p) − 1).

LaTeX

$$$ 0 < \operatorname{natDegree}(p) \Rightarrow \mathrm{nextCoeff}(p) = \operatorname{coeff}(p, \operatorname{natDegree}(p) - 1) $$$

Lean4

theorem nextCoeff_of_natDegree_pos (hp : 0 < p.natDegree) : nextCoeff p = p.coeff (p.natDegree - 1) :=
  by
  rw [nextCoeff, if_neg]
  contrapose! hp
  simpa

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

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

Разделы

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

Аффилиация

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