Theorems · Definition · number theory

PadicInt.continuousAddCharEquiv_of_norm_mul

(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] → [NormMulClass R] → { κ // Continuous ⇑κ } ≃ { r // ‖r‖ < 1 }

Equivalence between continuous additive characters ℤ_[p] → R, and r ∈ R with ‖r‖ < 1, for rings with strictly multiplicative norm.

Defined in

Mathlib.NumberTheory.Padics.AddChar

Cited by

2 results in Mathlib

Foundations

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

Assumes

FactNormedRingAlgebraIsBoundedSMulIsUltrametricDistCompleteSpaceNormMulClass