Theorem HahnSeries.leadingCoeff_nonpos_iff

Modification history

2025-06-16 07:16
Mathlib/RingTheory/HahnSeries/Lex.lean
feat(RingTheory/HahnSeries): equip HahnSeries with LinearOrder (#25168) …
Added HahnSeries.leadingCoeff_nonpos_iffView on Github →