isGalois — Mathlib

English

If k is a field and K is an algebraic closure of k (with CharZero k), then K/k is a Galois extension.

Русский

Если k — поле, а K — алгебраическое замыкание k (char 0), то K/k — галуа-расширение.

LaTeX

$$$\text{IsAlgClosure }(k,K) \wedge \operatorname{char}_0(k) \Rightarrow \ IsGalois(k,K)$$$

Lean4

instance (priority := 100) isGalois (k K : Type*) [Field k] [Field K] [Algebra k K] [IsAlgClosure k K] [CharZero k] :
    IsGalois k K where

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