Module

MixedCharPrincipalUnitLogScaling.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogScaling

2 declarations indexed from sourceView source ↗

Module documentation

Prime-power multiples in the principal-unit logarithm image

First multiply an arbitrary field element by a power of the residue prime to make it integral. The existing exponential construction then realizes an additional factor of p² as the logarithm of an actual principal unit.

Imports2

Imported by3

theorem

exists_principalUnit_log_eq_natCast_pow_mul

L24 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_principalUnit_log_eq_natCast_pow_mul

Documentation

Every field element has a prime-power multiple in the principal-unit logarithm image.

Source context 2 commands

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

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

Lean source · statement

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

theorem

exists_principalUnit_log_eq_natCast_pow_mul_ne_zero

L43 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_principalUnit_log_eq_natCast_pow_mul_ne_zero