add_of_left

Mathlib.Algebra.Polynomial.Monic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem add_of_left (hp : Monic p) (hpq : degree q < degree p) : Monic (p + q) := by
  rwa [Monic, add_comm, leadingCoeff_add_of_degree_lt hpq]

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

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

Разделы

Аффилиация

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