Structure HahnEmbedding.ArchimedeanStrata

Modification history

2025-09-14 09:24

Mathlib/Algebra/Order/Module/HahnEmbedding.lean

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

Added HahnEmbedding.ArchimedeanStrata View on Github →