Def HahnEmbedding.Seed.baseEmbedding

Modification history

2025-12-11 08:08
Mathlib/Algebra/Order/Module/HahnEmbedding.lean
chore: notation `R⟦Γ⟧ = HahnSeries Γ R` (#32670) …
Modified HahnEmbedding.Seed.baseEmbeddingView on Github →
2025-09-14 09:24
Mathlib/Algebra/Order/Module/HahnEmbedding.lean
feat(Algebra/Order): Hahn embedding theorem, part 1 (#27043) …
Added HahnEmbedding.Seed.baseEmbeddingView on Github →