Module

Complete.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.Complete

2 declarations indexed from sourceView source ↗

Module documentation

Complete nonarchimedean absolute values are Henselian

The localization reduction in the ramification-localization argument passes to the completion of a rank-one nonarchimedean absolute value. the factorization form of Hensel's lemma already supplies the degree-controlled factorization statement for every complete nonarchimedean absolute value. This file records the direct the primitive factorization definition consequence used in the henselianity criterion.

Imports2

Imported by11

theorem

henselFactorization_of_complete

L30 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_of_complete

Documentation

A complete nonarchimedean absolute value satisfies the factorization form of Hensel's lemma from the primitive factorization definition.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_of_complete
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) :
    ValuationTheory.DiscreteValuationField.HenselFactorizationProperty
      (absoluteValueValuationSubring v hnonarch)

theorem

henselianValuation_of_complete

L64 ↗

AlgebraicNumberTheory.Valuations.henselianValuation_of_complete