Theorem HahnEmbedding.Partial.archimedeanClassMk_le_of_eval_eq

Modification history

2025-09-14 09:24
Mathlib/Algebra/Order/Module/HahnEmbedding.lean
feat(Algebra/Order): Hahn embedding theorem, part 1 (#27043) …
Added HahnEmbedding.Partial.archimedeanClassMk_le_of_eval_eqView on Github →