Theorem Subsingleton.instDenselyOrdered

Modification history

2025-07-31 22:37

Mathlib/Order/Basic.lean

feat(Valued/LocallyCompact): do not require RankOne to show IsDVR (#27412) …

Modified Subsingleton.instDenselyOrdered View on Github →

2024-09-06 16:27

Mathlib/Order/Basic.lean

feat(Order/Hom): `denselyOrdered_iff_of_orderIsoClass` (#16427) …

Added Subsingleton.instDenselyOrdered View on Github →