English
The map f ↦ LSeries f is injective on the set of functions with f(0) = 0 and finite abscissa of absolute convergence.
Русский
Отображение f → LSeries f инъективно на множестве функций с f(0)=0 и конечной абсциссой абсолютной сходимости.
LaTeX
$$$$ \text{LSeries}_{|\{f : \mathbb{N} \to \mathbb{C} : f(0)=0 \land \operatorname{abscissaOfAbsConv}(f)<\top\}} \text{ is injective}. $$$$
Lean4
/-- The map `f ↦ LSeries f` is injective on functions `f` such that `f 0 = 0` and the L-series
of `f` converges somewhere. -/
theorem LSeries_injOn : Set.InjOn LSeries {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤} :=
by
intro f hf g hg h
simp only [Set.mem_setOf] at hf hg
replace h := (LSeries_eq_iff_of_abscissaOfAbsConv_lt_top hf.2 hg.2).mp h
ext1 n
cases n with
| zero => exact hf.1.trans hg.1.symm
| succ n => exact h _ n.zero_ne_add_one.symm
