Theorem HahnSeries.leadingCoeff_pos_iff

Modification history

2025-06-16 07:16

Mathlib/RingTheory/HahnSeries/Lex.lean

feat(RingTheory/HahnSeries): equip HahnSeries with LinearOrder (#25168) …

Added HahnSeries.leadingCoeff_pos_iff View on Github →