Theorem PowerSeries.exp_unique_of_derivative_eq_self

Modification history

2026-09-30 14:37
Mathlib/RingTheory/PowerSeries/Exp.lean
refactor(Algebra/Group): fix the definition of torsion-free non-abelian groups (#42407) …
Modified PowerSeries.exp_unique_of_derivative_eq_selfView on Github →
2026-01-23 10:44
Mathlib/RingTheory/PowerSeries/Exp.lean
feat(RingTheory/PowerSeries/Exp): more lemmas (#34265) …
Added PowerSeries.exp_unique_of_derivative_eq_selfView on Github →