English
If two power series representations of a function f at x exist with radii r1 and r2, then f has both representations on the ball of radius r2.
Русский
Если существуют две представления функции f через степенные ряды в точке x с радиусами r1 и r2, то f имеет оба представления на шаре радиуса r2.
LaTeX
$$$\\text{HasFPowerSeriesOnBall}\\, f\\, p_1\\, x\\, r_1 \\rightarrow \\text{HasFPowerSeriesOnBall}\\, f\\, p_2\\, x\\, r_2 \\rightarrow \\text{HasFPowerSeriesOnBall}\\, f\\, p_1\\, x\\, r_2.$$$
Lean4
/-- A one-dimensional formal multilinear series representing the zero function is zero. -/
theorem eq_zero {p : FormalMultilinearSeries 𝕜 𝕜 E} {x : 𝕜} (h : HasFPowerSeriesAt 0 p x) : p = 0 :=
by
ext n
rw [← mkPiRing_apply_one_eq_self (p n)]
simp [h.apply_eq_zero n 1]
