Theorems · Theorem · commutative algebra

PowerSeries.exp_unique_of_derivative_eq_self

∀ {A : Type u_3} [inst : CommRing A] [inst_1 : Algebra ℚ A] [IsAddTorsionFree A] {f : PowerSeries A},
  (PowerSeries.derivative A) f = f → PowerSeries.constantCoeff f = 1 → f = PowerSeries.exp A

A power series with derivative equal to itself and constant term 1 must be exp. The proof uses induction on coefficients: if f' = f and f(0) = 1, then coeff (n+1) f * (n+1) = coeff n f, which determines all coefficients uniquely.

Defined in

Mathlib.RingTheory.PowerSeries.Exp

Cited by

0 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAlgebraIsAddTorsionFree