Module

MixedCharPrincipalUnitLogLinearity.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogLinearity

1 declaration indexed from sourceView source ↗

Module documentation

P-adic linearity of the actual principal-unit logarithm

Both scalar actions and their continuity are supplied by the preceding constructions. Density of natural exponents upgrades additivity of the logarithm to linearity over the p-adic integers.

Imports5

Imported by4

theorem

principalUnitLogOfMixedChar_padicPow

L28 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogOfMixedChar_padicPow

Documentation

The logarithm takes a p-adic power to multiplication by that p-adic scalar.

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 principalUnitLogOfMixedChar_padicPow
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    (a : ℤ_[p])
    (x : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1) :
    (principalUnitLogOfMixedChar v p (principalUnitPadicPowOfMixedChar v p a x)).toAdd =
      padicIntToFieldOfMixedChar v p a * (principalUnitLogOfMixedChar v p x).toAdd

Module documentation

P-adic linearity of the actual principal-unit logarithm

Declarations

principalUnitLogOfMixedChar_padicPow