Theorem WithTop.coe_mono

Modification history

2026-02-10 13:35
Mathlib/Order/WithBot.lean
chore: cleanup using new `to_dual` capabilities (#34879) …
Deleted WithTop.coe_monoView on Github →
2025-12-28 23:05
Mathlib/Order/WithBot.lean
chore(Order/WithBot): use `to_dual` (part 4) (#33267)
Modified WithTop.coe_monoView on Github →
2024-01-23 09:49
Mathlib/Order/WithBot.lean
feat(Order/WithBot): add `WithBot.lt_coe_bot` (#9898) …
Modified WithTop.coe_monoView on Github →
2022-11-29 20:56
Mathlib/Order/WithBot.lean
feat: port Order.WithBot (#777) …
Added WithTop.coe_monoView on Github →