mathlib
287492c6 - refactor(ring_theory/hahn_series): non-linearly-ordered Hahn series (#7377)

Commit
4 years ago
refactor(ring_theory/hahn_series): non-linearly-ordered Hahn series (#7377) Refactors Hahn series to use `set.is_pwo` instead of `set.is_wf`, allowing them to be defined on non-linearly-ordered monomial types
Author
Parents
Loading