Theorem PowerSeries.derivative.ext

Modification history

2025-11-05 11:15

Mathlib/RingTheory/PowerSeries/Derivative.lean

chore: use `IsAddTorsionFree M` instead of `NoZeroSMulDivisors ℕ M`/`NoZeroSMulDivisors ℤ M` (#30683) …

Modified PowerSeries.derivative.ext View on Github →

2023-10-26 11:12

Mathlib/RingTheory/PowerSeries/Derivative.lean

feat (RingTheory/PowerSeries) add formal derivative operation (#7820) …

Added PowerSeries.derivative.ext View on Github →