Theorem HahnSeries.ofSuppBddBelow_zero

Modification history

2026-01-21 07:32

Mathlib/RingTheory/HahnSeries/Basic.lean

feat(RingTheory/HahnSeries/Basic): more theorems on `order`/`orderTop` (#33494) …

Added HahnSeries.ofSuppBddBelow_zero View on Github →