Theorem PowerSeries.deriv_log

Modification history

2026-08-30 09:00
Mathlib/RingTheory/PowerSeries/Log.lean
feat(RingTheory/PowerSeries/Log): log and exp as inverses (#37848) …
Deleted PowerSeries.deriv_logView on Github →
2026-04-09 09:56
Mathlib/RingTheory/PowerSeries/Log.lean
feat(PowerSeries): add barebones Log.lean (#36329)
Added PowerSeries.deriv_logView on Github →