Def HahnSeries.embDomainOrderEmbedding

Modification history

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