leadingCoeff_add_of_degree_lt'

Mathlib.Algebra.Polynomial.Degree.Operations

URI: https://scilib.ai/kg/mathlib#Polynomial.leadingCoeff_add_of_degree_lt'

← MathLib Explorer

English

If degree q < degree p, then leadingCoeff(p+q) = leadingCoeff p.

Русский

Если deg(q) < deg(p), то leadingCoeff(p+q) = leadingCoeff(p).

LaTeX

$$$degree(q) < degree(p) \Rightarrow leadingCoeff(p + q) = leadingCoeff(p)$$$

Lean4

theorem leadingCoeff_add_of_degree_lt' (h : degree q < degree p) : leadingCoeff (p + q) = leadingCoeff p :=
  by
  rw [add_comm]
  exact leadingCoeff_add_of_degree_lt h

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

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

Разделы

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

Аффилиация

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