uniqueGalXSubC

Mathlib.FieldTheory.PolynomialGaloisGroup

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

English

There is a unique Gal for the polynomial X - C x over F for each x in F.

Русский

Для полинома X - C x над F для каждого x в F существует уникальная Галуа.

LaTeX

$$$\forall x\in F:\; Unique\ (\;\, X - C x\;).Gal$$$

Lean4

instance uniqueGalXSubC (x : F) : Unique (X - C x).Gal :=
  uniqueGalOfSplits _ (splits_X_sub_C _)

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

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

Разделы

Аффилиация

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