Module

MixedCharPrincipalUnitLogImage.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogImage

1 declaration indexed from sourceView source ↗

Module documentation

The principal-unit logarithm contains the square of the residue prime

Exponentiating p² a for an element a of the valuation ring produces an actual principal unit with logarithm p² a. The convergence threshold is proved from the valuation of the residue prime. No normalized uniformizer, finite residue field, or restriction excluding the prime two is needed.

Imports3

Imported by3

theorem

exists_principalUnit_log_eq_natCast_sq_mul

L27 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_principalUnit_log_eq_natCast_sq_mul

Documentation

Every element of p² O is the logarithm of a first principal unit.

Source context 3 commands

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

namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u
variable {K : Type u} [Field K] [CharZero K]

Lean source · statement

theorem exists_principalUnit_log_eq_natCast_sq_mul
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    (a : v.valuationSubring) :
    ∃ u : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1,
      (principalUnitLogOfMixedChar v p u).toAdd = (p : K) ^ 2 * (a : K)

Module documentation

The principal-unit logarithm contains the square of the residue prime

Declarations

exists_principalUnit_log_eq_natCast_sq_mul