Theorems · Definition · number theory
PadicInt.addChar_of_value_at_one
{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] → (r : R) → Filter.Tendsto (fun x => r ^ x) Filter.atTop (nhds 0) → AddChar ℤ_[p] RThe unique continuous additive character of ℤ_[p] mapping 1 to 1 + r.
- Defined in
- Mathlib.NumberTheory.Padics.AddChar
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 217 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Algebrastatement and proof · cited by 11,388
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- Factstatement and proof · cited by 2,726
- CompleteSpacestatement and proof · cited by 2,532
- Filter.atTopstatement and proof · cited by 2,405
- Nat.Primestatement and proof · cited by 2,059
- NormedRingstatement and proof · cited by 924
- IsBoundedSMulstatement and proof · cited by 329
- AddCharstatement · cited by 286
- PadicIntstatement and proof · cited by 179
Cited by8
Results whose statement or proof uses this declaration.
- PadicInt.continuousAddCharEquivproof · cited by 2
- PadicInt.addChar_of_value_at_one_defstatement · cited by 1
- PadicInt.continuous_addChar_of_value_at_onestatement · cited by 1
- PadicInt.continuousAddCharEquiv_of_norm_mul_symm_applystatement · cited by 0
- PadicInt.continuousAddCharEquiv_symm_applystatement · cited by 0
- PadicInt.eq_addChar_of_value_at_onestatement · cited by 0
- PadicInt.coe_addChar_of_value_at_onestatement · cited by 0
- PadicInt.addChar_of_value_at_one.congr_simpstatement and proof · cited by 0