Theorem zero_lt_bit0

Modification history

2024-06-18 08:57

Mathlib/Algebra/Order/Ring/Defs.lean

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

Deleted zero_lt_bit0 View on Github →

2022-12-08 07:28

Mathlib/Algebra/Order/Ring/Defs.lean

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

Added zero_lt_bit0 View on Github →