Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subsingleton_iff_bot_eq_top

Modification history

2021-11-23 13:11
src/order/bounded_order.lean
refactor(*): split `order_{top,bot}` from `lattice` hierarchy (#9891) …
Modified subsingleton_iff_bot_eq_topView on Github →
2021-01-12 16:10
src/order/bounded_lattice.lean
feat(submonoid/basic): subsingleton and nontrivial instances for {add_,}submonoid (#5690)
Added subsingleton_iff_bot_eq_topView on Github →