of_mul_monic_left

Mathlib.Algebra.Polynomial.Monic

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

← MathLib Explorer

English

If p is monic and p·q is monic, then q is monic.

Русский

Если p моничен и p·q моничен, то q моничен.

LaTeX

$$$p\text{ Monic} \land (p\cdot q)\text{ Monic} \Rightarrow q\text{ Monic}.$$$

Lean4

theorem of_mul_monic_left (hp : p.Monic) (hpq : (p * q).Monic) : q.Monic :=
  by
  contrapose! hpq
  rw [Monic.def] at hpq ⊢
  rwa [leadingCoeff_monic_mul hp]

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

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

Разделы

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

Аффилиация

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