Theorem WithBot.one_eq_coe

Modification history

2024-07-17 15:24

Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

chore (Algebra.Order.WithTop): split into unbundled and bundled (#14531) …

Modified WithBot.one_eq_coe View on Github →

2024-01-09 09:25

Mathlib/Algebra/Order/Monoid/WithTop.lean

feat: More `WithBot` lemmas (#9580) …

Added WithBot.one_eq_coe View on Github →