Theorem MulArchimedeanClass.mk_le_mk_of_mabs

Modification history

2026-01-02 14:04
Mathlib/Algebra/Order/Archimedean/Class.lean
feat: `stdPart x = sSup {r | r < x}` (#33007)
Added MulArchimedeanClass.mk_le_mk_of_mabsView on Github →