Commit 2026-01-23 10:44 b8744879

View on Github →

feat(RingTheory/PowerSeries/Exp): more lemmas (#34265) Adds

  • PowerSeries.derivative_exp: The derivative of exp equals exp: d⁄dX A (exp A) = exp A.
  • PowerSeries.exp_unique_of_derivative_eq_self: A power series with derivative equal to itself and constant term 1 must be exp.
  • PowerSeries.isUnit_exp: exp A is a unit (invertible).
  • PowerSeries.order_exp: The order of exp A is 0.

Estimated changes

added theorem PowerSeries.isUnit_exp
added theorem PowerSeries.order_exp