Module

FinitelyGeneratedConsequences.lean

Nyll.Yamaguchi26AbfaithfulGalois.FieldExamples.FinitelyGeneratedConsequences

1 declaration indexed from sourceView source ↗

Module documentation

Imports4

Imported by2

theorem

Yamaguchi26AbfaithfulGalois.finitelyGenerated_isAbFaithful

Documentation

Every infinite finitely generated field is ab-faithful. The positive- characteristic case uses moving discrete valuations and local characters.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem finitelyGenerated_isAbFaithful
    (K : Type u) [Field K] [Infinite K] (hfg : Field.FG K) :
    IsAbFaithful Gal(AlgebraicClosure K/K)