isUnit_iff

Mathlib.Algebra.Polynomial.Monic

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

English

For a monic p, IsUnit p iff p = 1.

Русский

Для моноического p: IsUnit p тогда и только тогда p = 1.

LaTeX

$$$Monic(p) \Rightarrow (IsUnit(p) \leftrightarrow p = 1)$$$

Lean4

theorem isUnit_iff (hm : p.Monic) : IsUnit p ↔ p = 1 :=
  ⟨hm.eq_one_of_isUnit, fun h => h.symm ▸ isUnit_one⟩

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

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

Разделы

Аффилиация

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