of_mul_monic_right

Mathlib.Algebra.Polynomial.Monic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem of_mul_monic_right (hq : q.Monic) (hpq : (p * q).Monic) : p.Monic :=
  by
  contrapose! hpq
  rw [Monic.def] at hpq ⊢
  rwa [leadingCoeff_mul_monic hq]

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

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

Разделы

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

Аффилиация

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