splits_of_isUnit

Mathlib.Algebra.Polynomial.Splits

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

English

If u is a unit in K[X], then u.Splits i.

Русский

Если u единица в K[X], то u.Splits i.

LaTeX

$$IsUnit u → Splits i u$$

Lean4

theorem splits_of_isUnit [IsDomain K] {u : K[X]} (hu : IsUnit u) : u.Splits i :=
  (isUnit_iff.mp hu).choose_spec.2 ▸ splits_C _ _

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

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

Разделы

Аффилиация

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