isMulCommutative_galoisGroup

Mathlib.FieldTheory.Galois.Basic

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

← MathLib Explorer

English

The Galois group of a quadratic extension is abelian.

Русский

Галуа-группа квадратичного расширения абелева.

LaTeX

$$If $K/F$ is quadratic and Galois, then $\mathrm{Gal}(K/F)$ is abelian.$$

Lean4

/-- A quadratic extension has abelian Galois group.
-/
instance isMulCommutative_galoisGroup : IsMulCommutative (K ≃ₐ[F] K) :=
  ⟨IsCyclic.commutative⟩

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

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

Разделы

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

Аффилиация

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