Commit 2024-01-19 09:25 a86796b7

View on Github →

feat: Weaken an order hypothesis (#9849) The theorem as stated assumes LinearOrderedCancelAddCommMonoid Γ but the results used in the proof only need Zero Γ LinearOrder Γ

Estimated changes

Modified Mathlib/RingTheory/HahnSeries.lean

modified theorem HahnSeries.min_order_le_order_add