Module

FinitelyGeneratedCharZero.lean

Nyll.Yamaguchi26AbfaithfulGalois.FieldExamples.FinitelyGeneratedCharZero

1 declaration indexed from sourceView source ↗

Module documentation

The characteristic-zero case of the earlier finitely generated field example

The mixed-characteristic valuation is constructed from finite generation.

Imports3

Imported by2

theorem

finitelyGenerated_charZero_isAbFaithful

L24 ↗

Yamaguchi26AbfaithfulGalois.finitelyGenerated_charZero_isAbFaithful

Documentation

Finitely generated characteristic-zero fields are ab-faithful, by applying Theorem 3.6 to a discrete valuation constructed from an affine integer model.

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_charZero_isAbFaithful
    (K : Type u) [Field K] [CharZero K] (hfg : Field.FG K) :
    IsAbFaithful Gal(AlgebraicClosure K/K)

Module documentation

The characteristic-zero case of the earlier finitely generated field example

Declarations

finitelyGenerated_charZero_isAbFaithful