Theorems · Inductive type · field theory

IsAbelianGalois

(K : Type u_4) → (L : Type u_5) → [inst : Field K] → [inst_1 : Field L] → [Algebra K L] → Prop

The class of abelian extensions, defined as galois extensions whose galois group is commutative.

Defined in

Mathlib.FieldTheory.Galois.Abelian

Cited by

10 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

FieldFieldAlgebra