Theorem PowerSeries.coeff_of_lt_order_toNat

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_of_lt_order_toNatView on Github →
2025-04-16 20:00
Mathlib/RingTheory/PowerSeries/Order.lean
chore: cleanup API around order of univariate power series (#24072) …
Added PowerSeries.coeff_of_lt_order_toNatView on Github →