Theorem OrderDual.ofDual_eq_bot

Modification history

2025-11-18 16:33
Mathlib/Order/BoundedOrder/Basic.lean
feat: characterise regular elements of type synonyms (#31739)
Added OrderDual.ofDual_eq_botView on Github →