Commit 2024-07-16 00:30 8864f7cb
View on Github →refactor (RingTheory/HahnSeries/Summable) : Replace AddVal with orderTop (#14473)
To prepare for moving strictly valuation-theoretic material into a separate file, we replace the additive valuation with its underlying function in most places. This will allow us to remove unnecessary IsDomain R hypotheses in the future.