finGaloisGroup

Mathlib.FieldTheory.Galois.Profinite

URI: https://scilib.ai/kg/mathlib#FiniteGaloisIntermediateField.finGaloisGroup

← MathLib Explorer

English

The finite Galois group Gal(L/k) is a finite group.

Русский

Галуа-группа Gal(L/k) является конечной группой.

LaTeX

$$finGaloisGroup(L) : FiniteGrp$$

Lean4

/-- The (finite) Galois group `Gal(L / k)` associated to a
`L : FiniteGaloisIntermediateField k K` `L`. -/
def finGaloisGroup (L : FiniteGaloisIntermediateField k K) : FiniteGrp :=
  letI := AlgEquiv.fintype k L
  FiniteGrp.of <| L ≃ₐ[k] L

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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