English
If Nat.cast has dense range in A and κ1, κ2 are continuous AddChar A M with κ1(1)=κ2(1), then κ1=κ2.
Русский
Если Nat.cast имеет плотное покрытие в A и κ1, κ2 — непрерывные AddChar A M, причём κ1(1)=κ2(1), тогда κ1=κ2.
LaTeX
$$$\\text{DenseRange Nat.cast} \\Rightarrow \\forall {\\kappa_1\\kappa_2 : AddChar A M},\\;\\text{Continuous}(\\kappa_1) \\to \\text{Continuous}(\\kappa_2) \\to (\\kappa_1 1 = \\kappa_2 1) \\to \\kappa_1 = \\kappa_2$$$
Lean4
theorem addChar_eq_of_eval_one_eq {A M : Type*} [TopologicalSpace A] [AddMonoidWithOne A] [Monoid M]
[TopologicalSpace M] [T2Space M] (hdr : DenseRange ((↑) : ℕ → A)) {κ₁ κ₂ : AddChar A M} (hκ₁ : Continuous κ₁)
(hκ₂ : Continuous κ₂) (h : κ₁ 1 = κ₂ 1) : κ₁ = κ₂ :=
by
refine DFunLike.coe_injective <| hdr.equalizer hκ₁ hκ₂ (funext fun n ↦ ?_)
simp only [Function.comp_apply, ← nsmul_one, h, AddChar.map_nsmul_eq_pow]
