Theorems · Definition · number theory

PadicInt.mahlerEquiv

{p : ℕ} →
  [hp : Fact (Nat.Prime p)] →
    (E : Type u_1) →
      [inst : NormedAddCommGroup E] →
        [inst_1 : Module ℤ_[p] E] →
          [inst_2 : IsBoundedSMul ℤ_[p] E] →
            [IsUltrametricDist E] → [CompleteSpace E] → C(ℤ_[p], E) ≃ₗᵢ[ℤ_[p]] ZeroAtInftyContinuousMap ℕ E

The isometric equivalence from C(ℤ_[p], E) to the space of sequences in E tending to 0 given by Mahler's theorem, for E a nonarchimedean ℚ_[p]-Banach space.

Defined in

Mathlib.NumberTheory.Padics.MahlerBasis

Cited by

2 results in Mathlib

Foundations

Depth 218 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FactNormedAddCommGroupModuleIsBoundedSMulIsUltrametricDistCompleteSpace