Commit 2025-09-09 20:10 ed00a784

View on Github →

feat(RingTheory/HahnSeries): embDomain as OrderAddMonoidHom; orderTop of embDomain (#29421) These will be used in #27268 Hahn embedding theorem

Estimated changes