Theorem MvPowerSeries.lexOrder_zero

Modification history

2025-11-24 09:57
Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
chore: golf proofs that use `0 < x ↔ x ≠ 0` (#31895) …
Modified MvPowerSeries.lexOrder_zeroView on Github →
2024-09-18 22:25
Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
feat(MvPowerSeries.LexOrder): lexicographic order of multivariate power series (#14981) …
Added MvPowerSeries.lexOrder_zeroView on Github →