Theorem PowerSeries.coeff_order
Modification history
2025-08-21 10:55
Mathlib/RingTheory/PowerSeries/Order.lean
chore(RingTheory/(Mv)PowerSeries): use implicit parameters in `monomial`, `coeff`, `map`, `C`, and `constantCoeff` (#27889) …
Modified PowerSeries.coeff_orderView on Github →2025-04-16 20:00
Mathlib/RingTheory/PowerSeries/Order.lean
chore: cleanup API around order of univariate power series (#24072) …
Modified PowerSeries.coeff_orderView on Github →2024-12-01 10:47
Mathlib/RingTheory/PowerSeries/Order.lean
chore: remove PartENat from PowerSeries (#19622)
Modified PowerSeries.coeff_orderView on Github →