Module

Theorem4Dot2HigherLocalFields.lean

Nyll.Yamaguchi26AbfaithfulGalois.Theorem4Dot2HigherLocalFields

1 declaration indexed from sourceView source ↗

Module documentation

Theorem 4.2: ab-faithfulness of positive-dimensional higher local fields

Source: Yamaguchi, arXiv:2610.05634v1, Theorem 4.2. The stronger result including finiteness of roots is in HigherLocalField/Properties.lean.

Imports1

Nyll.Yamaguchi26AbfaithfulGalois.HigherLocalField.Properties

Imported by1

Nyll.Yamaguchi26AbfaithfulGalois.All

theorem

higher_local_field_abFaithful_4_2

L21 ↗

Yamaguchi26AbfaithfulGalois.higher_local_field_abFaithful_4_2

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
universe u v

Lean source · statement

theorem higher_local_field_abFaithful_4_2
    (n : ℕ) (K : Type u) [Field K]
    (hK : ValuationTheory.IsHigherLocalField.{u, v} n K) (hn : 0 < n) :
    IsAbFaithful Gal(AlgebraicClosure K/K)

Module documentation

Theorem 4.2: ab-faithfulness of positive-dimensional higher local fields

Declarations

higher_local_field_abFaithful_4_2