continuousAddCharEquiv_of_norm_mul_symm_apply

English

The symmetric form of the norm-multiplicative equivalence sends r with ‖r‖ < 1 to the corresponding additive char addChar_of_value_at_one r (tendsto_pow ...).

Русский

Обратная формa эквивалентности норм-муль переводит r с ‖r‖ < 1 к соответствующему аддитивному характеру addChar_of_value_at_one r (tendsto_pow ...).

LaTeX

$$$$ (\operatorname{continuousAddCharEquiv\_of\_norm\_mul p R)\,\text{symm}}\langle r, hr\rangle = \operatorname{addChar\_of\_value\_at\_one} r (\text{tendsto\_pow\_atTop\_nhds\_zero\_iff\_norm\_lt\_one.mpr } hr). $$$$

Lean4

@[simp]
theorem continuousAddCharEquiv_of_norm_mul_symm_apply {r : R} (hr : ‖r‖ < 1) :
    (continuousAddCharEquiv_of_norm_mul p R).symm ⟨r, hr⟩ =
      (addChar_of_value_at_one r (tendsto_pow_atTop_nhds_zero_iff_norm_lt_one.mpr hr) : AddChar ℤ_[p] R) :=
  rfl

Похожие утверждения