Module

SeparablyClosedResidue.lean

Nyll.Yamaguchi26AbfaithfulGalois.FieldExamples.SeparablyClosedResidue

1 declaration indexed from sourceView source ↗

Module documentation

Slimness with separably closed residue field

The separably-closed-residue corollary retained from the earlier manuscript. The residue field is required only to be separably closed.

Imports10

Imported by1

Nyll.Yamaguchi26AbfaithfulGalois.FieldExamples.All

theorem

mixedChar_separablyClosedResidue_finiteStepSolvable_slim

L32 ↗

Yamaguchi26AbfaithfulGalois.mixedChar_separablyClosedResidue_finiteStepSolvable_slim

Source context 4 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC ProCGroups.FiniteStepSolvableQuotients
open ValuationTheory.DiscreteValuationField
universe u v

Lean source · statement

theorem mixedChar_separablyClosedResidue_finiteStepSolvable_slim
    {K : Type u} [Field K] [CharZero K]
    (base : HenselianDVF.{u, v} K) (p : ℕ) [Fact p.Prime]
    [CharP base.residueField p] [IsSepClosed base.residueField] :
    ∀ m : ℕ, 2 ≤ m →
      IsSlim (MaxSolvQuot Gal(AlgebraicClosure K/K) m)

Module documentation

Slimness with separably closed residue field

Declarations

mixedChar_separablyClosedResidue_finiteStepSolvable_slim