Theorem HahnSeries.orderTop_embDomain

Modification history

2025-12-11 08:08
Mathlib/RingTheory/HahnSeries/Basic.lean
chore: notation `R⟦Γ⟧ = HahnSeries Γ R` (#32670) …
Modified HahnSeries.orderTop_embDomainView on Github →
2025-09-09 20:10
Mathlib/RingTheory/HahnSeries/Basic.lean
feat(RingTheory/HahnSeries): embDomain as OrderAddMonoidHom; orderTop of embDomain (#29421) …
Added HahnSeries.orderTop_embDomainView on Github →