Mathlib v3 is deprecated. Go to Mathlib v4

Theorem bit0_le_bit0

Modification history

2020-05-18 13:38
src/algebra/ordered_ring.lean
refactor(algebra): merge init_.algebra into algebra (#2707) …
Modified bit0_le_bit0View on Github →
2020-04-01 01:14
src/algebra/ordered_ring.lean
feat(data/nat/basic): `simp` lemmas about inequalities with `bit*` (#2207) …
Added bit0_le_bit0View on Github →