degree_sub_of_lt

Mathlib.RingTheory.MvPolynomial.MonomialOrder

URI: https://scilib.ai/kg/mathlib#MonomialOrder.degree_sub_of_lt

← MathLib Explorer

English

If deg(g) < deg(f) with respect to m, then deg(f - g) = deg(f).

Русский

Если deg(g) меньше deg(f) в порядке m, то deg(f - g) = deg(f).

LaTeX

$$$$ m.degree(g) \prec_m m.degree(f) \implies m.degree(f - g) = m.degree(f). $$$$

Lean4

theorem degree_sub_of_lt {f g : MvPolynomial σ R} (h : m.degree g ≺[m] m.degree f) : m.degree (f - g) = m.degree f :=
  by
  rw [sub_eq_add_neg]
  apply degree_add_of_lt
  simp only [degree_neg, h]

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

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

Разделы

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

Аффилиация

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