mathlib
1b0db8e3 - feat(order/well_founded_set, ring_theory/hahn_series): `hahn_series.add_val` (#6564)

Commit
4 years ago
feat(order/well_founded_set, ring_theory/hahn_series): `hahn_series.add_val` (#6564) Defines `set.is_wf.min` in terms of `well_founded.min` Places an `add_valuation`, `hahn_series.add_val`, on `hahn_series` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Author
Parents
Loading