Mathlib v3 is deprecated. Go to Mathlib v4

Theorem one_lt_bit1

Modification history

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