isGalois_bot

Mathlib.FieldTheory.Galois.Basic

URI: https://scilib.ai/kg/mathlib#isGalois_bot

English

If E/F is Galois and Aut(E/F) is finite, then E is finite-dimensional over F.

Русский

Если E/F Галуа и Aut(E/F) конечна, тогда E конечномодульно над F.

LaTeX

$$FiniteDimensional F E$$

Lean4

instance isGalois_bot : IsGalois F (⊥ : IntermediateField F E) :=
  (IntermediateField.botEquiv F E).transfer_galois.mpr (IsGalois.self F)

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

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

Разделы

Аффилиация

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