Theorem HahnSeries.leadingCoeff_neg

Modification history

2025-06-16 07:16

Mathlib/RingTheory/HahnSeries/Addition.lean

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

Added HahnSeries.leadingCoeff_neg View on Github →