Theorem MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero

Modification history

2024-09-18 22:25
Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
feat(MvPowerSeries.LexOrder): lexicographic order of multivariate power series (#14981) …
Added MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zeroView on Github →