Module

PadicFiniteTypeRoots.lean

Nyll.Yamaguchi26AbfaithfulGalois.FieldExamples.PadicFiniteTypeRoots

3 declarations indexed from sourceView source ↗

Module documentation

Roots of unity in finitely generated p-adic extensions

Finite extensions of the p-adic field have finite torsion unit groups. The same finiteness holds in essentially finite-type extensions by passing to their finite extension of algebraic constants.

Imports6

Imported by2

theorem

padicCompleteDVF_residue_char

L26 ↗

Yamaguchi26AbfaithfulGalois.padicCompleteDVF_residue_char

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
universe u

Lean source · statement

theorem padicCompleteDVF_residue_char (p : ℕ) [Fact p.Prime] :
    CharP (padicCompleteDVF p).residueField p

theorem

finite_torsion_finiteExtension_padic

L33 ↗

Yamaguchi26AbfaithfulGalois.finite_torsion_finiteExtension_padic

Documentation

Finite extensions of Q_p have finite torsion units, via their actual residue field.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
universe u

Lean source · statement

theorem finite_torsion_finiteExtension_padic
    (p : ℕ) [Fact p.Prime] (C : Type u) [Field C] [Algebra (Padic p) C]
    [FiniteDimensional (Padic p) C] : Finite (CommGroup.torsion Cˣ)

theorem

finite_torsion_of_essFiniteType_padic

L51 ↗

Yamaguchi26AbfaithfulGalois.finite_torsion_of_essFiniteType_padic

Documentation

Roots of unity in a finitely generated Q_p-extension lie in its finite extension of algebraic constants.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
universe u

Lean source · statement

theorem finite_torsion_of_essFiniteType_padic
    (p : ℕ) [Fact p.Prime] (E : Type u) [Field E] [Algebra (Padic p) E]
    [Algebra.EssFiniteType (Padic p) E] : Finite (CommGroup.torsion Eˣ)

Module documentation

Roots of unity in finitely generated p-adic extensions

Declarations

padicCompleteDVF_residue_char

finite_torsion_finiteExtension_padic

finite_torsion_of_essFiniteType_padic