English
If two power-series have the same derivative and the same constant term, then they are equal.
Русский
Если два степенных ряда имеют одинаковую производную и одинаковый константный член, то они равны.
LaTeX
$$$ \\text{If } d/dX f = d/dX g \\text{ and } \\operatorname{constantCoeff}(f) = \\operatorname{constantCoeff}(g) \\text{ then } f=g$$$
Lean4
/-- If `f` and `g` have the same constant term and derivative, then they are equal. -/
theorem ext {R} [CommRing R] [NoZeroSMulDivisors ℕ R] {f g} (hD : d⁄dX R f = d⁄dX R g)
(hc : constantCoeff f = constantCoeff g) : f = g := by
ext n
cases n with
| zero => rw [coeff_zero_eq_constantCoeff, hc]
| succ n =>
have equ : coeff n (d⁄dX R f) = coeff n (d⁄dX R g) := by rw [hD]
rwa [coeff_derivative, coeff_derivative, ← cast_succ, mul_comm, ← nsmul_eq_mul, mul_comm, ← nsmul_eq_mul,
smul_right_inj n.succ_ne_zero] at equ
