Theorem HahnSeries.order_mul_of_ne_zero

Modification history

2026-01-02 22:26
Mathlib/RingTheory/HahnSeries/Multiplication.lean
feat: `IsStrictOrderedRing (Lex R⟦Γ⟧)` (#33398) …
Added HahnSeries.order_mul_of_ne_zeroView on Github →