degree_add_eq_right_of_lt

Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

← MathLib Explorer

English

If deg f ≺ deg g, then deg(f+g) = deg g.

Русский

Если deg f меньше deg g, то deg(f+g) = deg g.

LaTeX

$$$m.degree f \prec_m m.degree g \Rightarrow m.degree (f+g) = m.degree g$$$

Lean4

theorem degree_add_eq_right_of_lt {f g : MvPolynomial σ R} (h : m.degree f ≺[m] m.degree g) :
    m.degree (f + g) = m.degree g := by
  rw [add_comm]
  exact degree_add_of_lt h

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

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

Разделы

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

Аффилиация

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