Theorem HahnSeries.leadingCoeff_abs

Modification history

2025-06-16 07:16

Mathlib/RingTheory/HahnSeries/Lex.lean

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

Added HahnSeries.leadingCoeff_abs View on Github →