eq_of_monic_of_associated

Mathlib.Algebra.Polynomial.Monic

URI: https://scilib.ai/kg/mathlib#Polynomial.eq_of_monic_of_associated

← MathLib Explorer

English

If p and q are monic and Associated, then p = q.

Русский

Если p и q моноичны и эквивалентны по ассоциации, то p = q.

LaTeX

$$$Monic(p) \land Monic(q) \land Associated(p,q) \Rightarrow p = q$$$

Lean4

theorem eq_of_monic_of_associated (hp : p.Monic) (hq : q.Monic) (hpq : Associated p q) : p = q :=
  by
  obtain ⟨u, rfl⟩ := hpq
  rw [(hp.of_mul_monic_left hq).eq_one_of_isUnit u.isUnit, mul_one]

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

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

Разделы

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

Аффилиация

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