add_of_right

Mathlib.Algebra.Polynomial.Monic

URI: https://scilib.ai/kg/mathlib#Polynomial.Monic.add_of_right

English

If q is monic and deg p < deg q, then p + q is monic.

Русский

Если q моничен и deg p < deg q, то p + q моничен.

LaTeX

$$$q\text{ monic} \land \deg p < \deg q \Rightarrow p+q\text{ Monic}.$$$

Lean4

theorem add_of_right (hq : Monic q) (hpq : degree p < degree q) : Monic (p + q) := by
  rwa [Monic, leadingCoeff_add_of_degree_lt hpq]

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

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

Разделы

Аффилиация

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