Theorem bit1_lt_bit1

Modification history

2024-06-18 08:57

Mathlib/Algebra/Order/Ring/Defs.lean

chore(*): drop `bit*_mono` (#13914)

Deleted bit1_lt_bit1 View on Github →

2022-12-08 07:28

Mathlib/Algebra/Order/Ring/Defs.lean

feat: port Algebra.Order.[Ring|Field].Defs (#905) …

Added bit1_lt_bit1 View on Github →