Def HahnEmbedding.Partial.toOrderAddMonoidHom

Modification history

2025-12-11 08:08

Mathlib/Algebra/Order/Module/HahnEmbedding.lean

chore: notation `R⟦Γ⟧ = HahnSeries Γ R` (#32670) …

Modified HahnEmbedding.Partial.toOrderAddMonoidHom View on Github →

2025-09-14 09:24

Mathlib/Algebra/Order/Module/HahnEmbedding.lean

feat(Algebra/Order): Hahn embedding theorem, part 1 (#27043) …

Added HahnEmbedding.Partial.toOrderAddMonoidHom View on Github →