Theorem WithBot.coe_bit1

Modification history

2024-06-10 07:27
Mathlib/Algebra/Order/Monoid/WithTop.lean
chore(*): drop some bit0/bit1 lemmas (#13679) …
Deleted WithBot.coe_bit1View on Github →
2023-01-07 14:35
Mathlib/Algebra/Order/Monoid/WithTop.lean
chore: tidy various files (#1412)
Added WithBot.coe_bit1View on Github →