self_sub_monomial_natDegree_leadingCoeff

Mathlib.Algebra.Polynomial.EraseLead

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

← MathLib Explorer

English

Subtracting the leading monomial from f yields its eraseLead.

Русский

Вычитание ведущего монома из f даёт eraseLead(f).

LaTeX

$$f - monomial(f.natDegree) f.leadingCoeff = f.eraseLead$$

Lean4

@[simp]
theorem self_sub_monomial_natDegree_leadingCoeff {R : Type*} [Ring R] (f : R[X]) :
    f - monomial f.natDegree f.leadingCoeff = f.eraseLead :=
  (eq_sub_iff_add_eq.mpr (eraseLead_add_monomial_natDegree_leadingCoeff f)).symm

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

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

Разделы

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

Аффилиация

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