Theorems · Definition · commutative algebra
PowerSeries.derivativeFun
Deprecated since 2026-06-26Use PowerSeries.derivative instead.
{R : Type u_1} → [CommSemiring R] → PowerSeries R → PowerSeries RThe formal derivative of a power series in one variable.
This is defined here as a function, but will be packaged as a
derivation derivative on R⟦X⟧.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- PowerSeriesstatement and proof · cited by 797
- AddHom.toFunproof · cited by 168
- LinearMap.toAddHomproof · cited by 165
- PowerSeries.derivativeproof · cited by 26
- Derivation.toLinearMapproof · cited by 21
Cited by4
Results whose statement or proof uses this declaration.
- PowerSeries.derivativeFun_smulstatement · cited by 0
- PowerSeries.derivativeFun_addstatement · cited by 0
- PowerSeries.derivativeFun_mulstatement · cited by 0
- PowerSeries.derivativeFun_onestatement · cited by 0