uniqueGalC

Mathlib.FieldTheory.PolynomialGaloisGroup

URI: https://scilib.ai/kg/mathlib#Polynomial.Gal.uniqueGalC

English

There is a unique Gal for the polynomial C x, i.e., constants yield unique Gal.

Русский

Для полинома Cx существует уникальная Galalgia.

LaTeX

$$$\text{instance } Unique (\mathrm{Polynomial.Gal}\; C x)$$$

Lean4

instance uniqueGalC (x : F) : Unique (C x).Gal :=
  uniqueGalOfSplits _ (splits_C _ _)

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

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

Разделы

Аффилиация

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