Theorems · Definition · number theory

PadicInt.continuousAddCharEquiv

(p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (R : Type u_1) →
      [inst_1 : NormedRing R] →
        [inst_2 : Algebra ℤ_[p] R] →
          [IsBoundedSMul ℤ_[p] R] →
            [IsUltrametricDist R] →
              [CompleteSpace R] →
                { κ // Continuous ⇑κ } ≃ { r // Filter.Tendsto (fun x => r ^ x) Filter.atTop (nhds 0) }

Equivalence between continuous additive characters ℤ_[p] → R, and r ∈ R with r ^ n → 0.

Defined in

Mathlib.NumberTheory.Padics.AddChar

Cited by

2 results in Mathlib

Foundations

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

Assumes

FactNormedRingAlgebraIsBoundedSMulIsUltrametricDistCompleteSpace