Theorem HahnSeries.orderTop_add_orderTop_le_orderTop_mul

Modification history

2025-08-14 21:19
Mathlib/RingTheory/HahnSeries/Multiplication.lean
chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (#28231) …
Deleted HahnSeries.orderTop_add_orderTop_le_orderTop_mulView on Github →
2025-04-04 17:16
Mathlib/RingTheory/HahnSeries/Multiplication.lean
chore: use mixin ordered algebraic typeclasses (part 1) (#20594)
Modified HahnSeries.orderTop_add_orderTop_le_orderTop_mulView on Github →
2024-07-16 00:30
Mathlib/RingTheory/HahnSeries/Multiplication.lean
refactor (RingTheory/HahnSeries/Summable) : Replace AddVal with orderTop (#14473) …
Added HahnSeries.orderTop_add_orderTop_le_orderTop_mulView on Github →