isGalois

Mathlib.FieldTheory.Galois.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.IsQuadraticExtension.isGalois

English

A quadratic separable extension is Galois.

Русский

Квадратичное разделимое расширение гало.

LaTeX

$$$[K:F] = 2$ и $K/F$ сепарабельное ⇒ K/F is Galois.$$

Lean4

/-- A quadratic separable extension is Galois.
-/
instance isGalois [Algebra.IsSeparable F K] : IsGalois F K where

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

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

Разделы

Аффилиация

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