continuousAddCharEquiv_symm_apply

English

The inverse of the equivalence sends r with hr to the additive character addChar_of_value_at_one r hr.

Русский

Обратное отображение эквивалентности переводит r с hr в аддитивный характер addChar_of_value_at_one r hr.

LaTeX

$$$$ (\text{continuousAddCharEquiv}(p,R))^{-1} \langle r,hr\rangle = \bigl( \operatorname{addChar\_of\_value\_at\_one} r hr : \mathrm{AddChar}(\mathbb{Z}_p,R)\bigr). $$$$

Lean4

@[simp]
theorem continuousAddCharEquiv_symm_apply {r : R} (hr : Tendsto (r ^ ·) atTop (𝓝 0)) :
    (continuousAddCharEquiv p R).symm ⟨r, hr⟩ = (addChar_of_value_at_one r hr : AddChar ℤ_[p] R) :=
  rfl

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