Mathlib Changelog
v4
Changelog
About
Github
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_embDomain
View 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_embDomain
View on Github →