uniqueGalOne

Mathlib.FieldTheory.PolynomialGaloisGroup

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

English

Proof that the zero polynomial has a unique Galois group; the splitting is trivial.

Русский

Доказательство того, что нулевой многочлен имеет тривиальную группу Галуа; разложение тривиально.

LaTeX

$$$\text{proof of } \text{Unique}(\mathrm{Gal}_0)$.$$

Lean4

instance uniqueGalOne : Unique (1 : F[X]).Gal :=
  uniqueGalOfSplits _ (splits_one _)

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

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

Разделы

Аффилиация

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