Theorems · Definition · commutative algebra
PowerSeries
Type u_1 → Type (max u_1 0)
Formal power series over a coefficient type R
- Defined in
- Mathlib.RingTheory.PowerSeries.Basic
- Cited by
- 797 results in Mathlib
- Foundations
- Depth 19 from the axioms, rests on 114 definitions · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MvPowerSeriesproof · cited by 659
Cited by899
Results whose statement or proof uses this declaration.
- PowerSeries.coeffstatement · cited by 324
- PowerSeries.Xstatement · cited by 183
- PowerSeries.constantCoeffstatement · cited by 126
- Polynomial.toPowerSeriesstatement · cited by 96
- PowerSeries.orderstatement and proof · cited by 92
- PowerSeries.mapstatement · cited by 82
- PowerSeries.Cstatement · cited by 76
- PowerSeries.extstatement and proof · cited by 69
- UpperHalfPlane.qExpansionstatement · cited by 64
- PowerSeries.subststatement and proof · cited by 58
- PowerSeries.mkstatement · cited by 52
- PowerSeries.coeff_mkstatement · cited by 47
Showing the 200 most cited of 899.