Theorem HahnSeries.orderTop_of_Subsingleton

Modification history

2025-08-19 23:16
Mathlib/RingTheory/HahnSeries/Basic.lean
chore(HahnSeries): make more usable, golf (#28632) …
Deleted HahnSeries.orderTop_of_SubsingletonView on Github →
2025-02-17 03:56
Mathlib/RingTheory/HahnSeries/Basic.lean
feat (RingTheory/HahnSeries): algebra homomorphism from PowerSeries to HahnSeries. (#21313) …
Added HahnSeries.orderTop_of_SubsingletonView on Github →