instUniqueOfFactSplitsId

Mathlib.FieldTheory.PolynomialGaloisGroup

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

English

If p splits over F, then the Galois group Gal(p) is unique (trivial).

Русский

Если p делится над F, то группа Галуа Gal(p) единственна (тривиальна).

LaTeX

$$$\text{instance } [h:\mathrm{Fact}(p\;\mathrm{Splits}(\mathrm{id}_F))] : \mathrm{Unique}\ p.Gal$$$

Lean4

instance [h : Fact (p.Splits (RingHom.id F))] : Unique p.Gal :=
  uniqueGalOfSplits _ h.1

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

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

Разделы

Аффилиация

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