add_of_lt

Mathlib.RingTheory.MvPolynomial.MonomialOrder

URI: https://scilib.ai/kg/mathlib#MonomialOrder.Monic.add_of_lt

← MathLib Explorer

English

If f is monic and deg g ≺ deg f, then f+g is monic.

Русский

Если f моническое, а deg g ⪯ deg f, то f+g моническое.

LaTeX

$$m.Monic f \to + (m.degree g) ≺ m.degree f) ⇒ m.Monic (f+g)$$

Lean4

theorem add_of_lt {f g : MvPolynomial σ R} (hf : m.Monic f) (h : m.degree g ≺[m] m.degree f) : m.Monic (f + g) := by
  simp only [Monic, leadingCoeff_add_of_lt h, hf.leadingCoeff_eq_one]

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

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

Разделы

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

Аффилиация

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