Commit 2025-08-14 21:19 fcb588c2
View on Github →chore(RingTheory/HahnSeries): deprecate duplicate orderTop_add_orderTop_le_orderTop_mul (#28231)
Motivation: Avoid duplication.
chore(RingTheory/HahnSeries): deprecate duplicate orderTop_add_orderTop_le_orderTop_mul (#28231)
Motivation: Avoid duplication.