eq_addChar_of_value_at_one — Mathlib

English

If κ is any continuous additive character with κ(1) = 1 + r, then κ must be the unique character defined by addChar_of_value_at_one r hr.

Русский

Если κ — непрерывный аддитивный характер с κ(1)=1+r, то κ является единственным характером, заданным через addChar_of_value_at_one r hr.

LaTeX

$$$$\forall\kappa\;\bigl(\text{Continuous}(\kappa) \wedge \kappa(1)=1+r\bigr)\Rightarrow \kappa=\operatorname{addChar\_of\_value\_at\_one}(r,hr).$$$$

Lean4

theorem eq_addChar_of_value_at_one {r : R} (hr : Tendsto (r ^ ·) atTop (𝓝 0)) {κ : AddChar ℤ_[p] R} (hκ : Continuous κ)
    (hκ' : κ 1 = 1 + r) : κ = addChar_of_value_at_one r hr :=
  denseRange_natCast.addChar_eq_of_eval_one_eq hκ (by fun_prop) (by simp [hκ'])

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