NYLL
Module

CompletedPrimitiveUniformizer.lean

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedPrimitiveUniformizer
12 declarations indexed from sourceView source ↗

Module documentation

The completed p-adic primitive point is a uniformizer

The primitive multiplicative Lubin--Tate polynomial remains Eisenstein over the completed-unramified valuation ring. This file uses that actual Eisenstein equation and the fundamental ramification identity to prove that the chosen completed primitive point has normalized additive valuation one. Consequently it is a genuine uniformizer of the completed level.

Imports3
Imported by3

Declarations

instance

padicCompletedPrimitiveUniformizerTargetWithIdeal

L35 ↗
LubinTate.padicCompletedPrimitiveUniformizerTargetWithIdeal
Source context 8 commands

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

noncomputable section
open scoped Polynomial Topology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · full declaration
instance
    padicCompletedPrimitiveUniformizerTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
instance

padicCompletedPrimitiveUniformizerTargetCompleteSpace

L42 ↗
LubinTate.padicCompletedPrimitiveUniformizerTargetCompleteSpace
Source context 9 commands

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

noncomputable section
open scoped Polynomial Topology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
Lean source · statement
instance
    padicCompletedPrimitiveUniformizerTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring
instance

padicCompletedPrimitiveUniformizerTargetT2Space

L51 ↗
LubinTate.padicCompletedPrimitiveUniformizerTargetT2Space
Source context 10 commands

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

noncomputable section
open scoped Polynomial Topology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
Lean source · statement
instance
    padicCompletedPrimitiveUniformizerTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring
theorem

completedPolynomial_eval₂_mem_ideal_of_coeff_mem

L60 ↗
LubinTate.completedPolynomial_eval₂_mem_ideal_of_coeff_mem
Source context 11 commands

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

noncomputable section
open scoped Polynomial Topology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem completedPolynomial_eval₂_mem_ideal_of_coeff_mem
    {R S : Type*} [CommSemiring R] [CommSemiring S]
    (f : R →+* S) (I : Ideal S) (P : Polynomial R) (z : S)
    (hcoeff : ∀ i, f (P.coeff i) ∈ I) :
    P.eval₂ f z ∈ I
theorem

padicCompletedPrimitiveRootInteger_addVal_and_ramificationIndex

L69 ↗
LubinTate.padicCompletedPrimitiveRootInteger_addVal_and_ramificationIndex
Source context 11 commands

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

noncomputable section
open scoped Polynomial Topology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem
    padicCompletedPrimitiveRootInteger_addVal_and_ramificationIndex
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    IsDiscreteValuationRing.addVal
        (padicCompletedLevelCompleteDVF p n).valuationSubring
        (padicCompletedPrimitiveRootInteger p n) = 1 ∧
      ramificationIndex
          (padicCompletedUnramifiedCompleteDVF p).toDVF
          (padicCompletedLevelCompleteDVF p n).toDVF =
        degree
          (padicCompletedUnramifiedCompleteDVF p).toDVF
          (padicCompletedLevelCompleteDVF p n).toDVF
theorem

padicCompletedPrimitiveRootInteger_addVal

L343 ↗
LubinTate.padicCompletedPrimitiveRootInteger_addVal
Documentation

The chosen completed primitive point has normalized additive valuation one in the completed-level valuation ring.

Source context 11 commands

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

noncomputable section
open scoped Polynomial Topology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRootInteger_addVal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    IsDiscreteValuationRing.addVal
        (padicCompletedLevelCompleteDVF p n).valuationSubring
        (padicCompletedPrimitiveRootInteger p n) = 1
theorem

padicCompletedLevel_ramificationIndex_eq_degree

L353 ↗
LubinTate.padicCompletedLevel_ramificationIndex_eq_degree
Documentation

The completed multiplicative Lubin--Tate level is totally ramified over the completed-unramified coefficient field.

Source context 11 commands

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

noncomputable section
open scoped Polynomial Topology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedLevel_ramificationIndex_eq_degree
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    ramificationIndex
        (padicCompletedUnramifiedCompleteDVF p).toDVF
        (padicCompletedLevelCompleteDVF p n).toDVF =
      degree
        (padicCompletedUnramifiedCompleteDVF p).toDVF
        (padicCompletedLevelCompleteDVF p n).toDVF
theorem

padicCompletedPrimitiveRootInteger_irreducible

L366 ↗
LubinTate.padicCompletedPrimitiveRootInteger_irreducible
Documentation

The completed primitive point is irreducible in the completed-level valuation ring.

Source context 11 commands

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

noncomputable section
open scoped Polynomial Topology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRootInteger_irreducible
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Irreducible (padicCompletedPrimitiveRootInteger p n)
theorem

padicCompletedPrimitiveRoot_isUniformizer

L384 ↗
LubinTate.padicCompletedPrimitiveRoot_isUniformizer
Documentation

The chosen completed primitive point is a genuine uniformizer of the completed level.

Source context 11 commands

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

noncomputable section
open scoped Polynomial Topology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRoot_isUniformizer
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedLevelCompleteDVF p n).valuation.IsUniformizer
      (padicCompletedPrimitiveRootInteger p n :
        padicCompletedLevelField p n)
theorem

padicChangedUniformizerThetaValue_addVal_and_ramificationIndex

L393 ↗
LubinTate.padicChangedUniformizerThetaValue_addVal_and_ramificationIndex
Source context 11 commands

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

noncomputable section
open scoped Polynomial Topology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem
    padicChangedUniformizerThetaValue_addVal_and_ramificationIndex
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IsDiscreteValuationRing.addVal
        (padicCompletedLevelCompleteDVF p n).valuationSubring
        (padicChangedUniformizerThetaValue p u n) = 1 ∧
      ramificationIndex
          (padicCompletedUnramifiedCompleteDVF p).toDVF
          (padicCompletedLevelCompleteDVF p n).toDVF =
        (p - 1) * p ^ n
theorem

padicChangedUniformizerThetaValue_addVal

L669 ↗
LubinTate.padicChangedUniformizerThetaValue_addVal
Documentation

The genuine changed-uniformizer theta point has normalized additive valuation one in the completed standard level.

Source context 11 commands

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

noncomputable section
open scoped Polynomial Topology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicChangedUniformizerThetaValue_addVal
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IsDiscreteValuationRing.addVal
        (padicCompletedLevelCompleteDVF p n).valuationSubring
        (padicChangedUniformizerThetaValue p u n) = 1
theorem

padicChangedUniformizerThetaValue_isUniformizer

L680 ↗
LubinTate.padicChangedUniformizerThetaValue_isUniformizer
Documentation

The genuine changed-uniformizer theta point is a uniformizer of the completed standard level.

Source context 11 commands

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

noncomputable section
open scoped Polynomial Topology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedPrimitiveUniformizerTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicChangedUniformizerThetaValue_isUniformizer
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicCompletedLevelCompleteDVF p n).valuation.IsUniformizer
      ((padicChangedUniformizerThetaValue p u n :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
          padicCompletedLevelField p n)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.