eraseLead

Mathlib.Algebra.Polynomial.EraseLead

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

← MathLib Explorer

English

EraseLead f is the polynomial obtained by subtracting from f its leading term.

Русский

EraseLead f— это многочлен, получаемый вычитанием из f его ведущего членa.

LaTeX

$$EraseLead(f) = f - (leadingTerm of f)$$

Lean4

/-- `eraseLead f` for a polynomial `f` is the polynomial obtained by
subtracting from `f` the leading term of `f`. -/
def eraseLead (f : R[X]) : R[X] :=
  Polynomial.erase f.natDegree f

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

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

Разделы

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

Аффилиация

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