Theorems · Theorem · commutative algebra
PowerSeries.derivative_invOf
∀ {R : Type u_1} [inst : CommRing R] (f : PowerSeries R) [inst_1 : Invertible f],
(PowerSeries.derivative R) ⅟f = -⅟f ^ 2 * (PowerSeries.derivative R) f- Cited by
- 0 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingInvertible
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- PowerSeriesstatement and proof · cited by 797
- Invertiblestatement and proof · cited by 549
- Derivationstatement · cited by 293
- Invertible.invOfstatement · cited by 268
- PowerSeries.derivativestatement · cited by 26
- MvPowerSeries.pderiv_invOfproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.