Theorem HahnSeries.orderTop_eq_of_le

Modification history

2025-12-11 08:08
Mathlib/RingTheory/HahnSeries/Basic.lean
chore: notation `R⟦Γ⟧ = HahnSeries Γ R` (#32670) …
Modified HahnSeries.orderTop_eq_of_leView on Github →
2024-11-13 21:29
Mathlib/RingTheory/HahnSeries/Basic.lean
feat(Order/WellFoundedSet): sufficient conditions for unique minima of well-founded sets (#18977) …
Added HahnSeries.orderTop_eq_of_leView on Github →