Commit 2026-01-21 07:32 7b9235af

View on Github →

feat(RingTheory/HahnSeries/Basic): more theorems on order/orderTop (#33494) We also deprecate various badly named or overspecific theorems relating to ofSuppBddBelow.

Estimated changes

Modified Mathlib/Algebra/Vertex/VertexOperator.lean

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

added theorem HahnSeries.coeff_ofSuppBddBelow

added theorem HahnSeries.le_orderTop_iff_forall

added theorem HahnSeries.le_order_iff_forall

modified def HahnSeries.ofSuppBddBelow

added theorem HahnSeries.ofSuppBddBelow_eq_zero

added theorem HahnSeries.ofSuppBddBelow_zero

added theorem HahnSeries.orderTop_lt_iff_exists

added theorem HahnSeries.order_lt_iff_exists

deleted theorem HahnSeries.zero_ofSuppBddBelow

Modified Mathlib/RingTheory/LaurentSeries.lean