Theorem HahnEmbedding.ArchimedeanStrata.ball_eq_closedBall

Modification history

2026-01-16 16:52
Mathlib/Algebra/Order/Module/HahnEmbedding.lean
refactor(Algebra/Order): change `MulArchimedeanClass.subgroup` to `FiniteArchimedeanClass.subgroup` (#32886) …
Deleted HahnEmbedding.ArchimedeanStrata.ball_eq_closedBallView on Github →
2025-09-14 09:24
Mathlib/Algebra/Order/Module/HahnEmbedding.lean
feat(Algebra/Order): Hahn embedding theorem, part 1 (#27043) …
Added HahnEmbedding.ArchimedeanStrata.ball_eq_closedBallView on Github →