English
There is an equivalence between continuous additive characters and r ∈ R with ‖r‖ < 1, given by κ ↦ κ(1) − 1 and r ↦ addChar_of_value_at_one r hr.
Русский
Существует эквиваленция между непрерывными аддитивными характерами и элементами r с ‖r‖ < 1, задаваемая κ ↦ κ(1) − 1 и r ↦ addChar_of_value_at_one r hr.
LaTeX
$$$$\{ \kappa:\mathrm{AddChar}(\mathbb{Z}_p,R)\mid \mathrm{Continuous}(\kappa) \} \cong \{ r\in R\mid \|r\|<1 \}.$$$$
Lean4
/-- Equivalence between continuous additive characters `ℤ_[p] → R`, and `r ∈ R` with `‖r‖ < 1`,
for rings with strictly multiplicative norm. -/
noncomputable def continuousAddCharEquiv_of_norm_mul : { κ : AddChar ℤ_[p] R // Continuous κ } ≃ { r : R // ‖r‖ < 1 } :=
(continuousAddCharEquiv p R).trans <| .subtypeEquivProp (by simp only [tendsto_pow_atTop_nhds_zero_iff_norm_lt_one])
