Commit 2022-06-02 21:38 1a1895cd

View on Github →

feat(data/nat/basic): add lemmas about nat.bit_cases_on (#14481) Also drop nat.bit_cases (was the same definition with a different order of arguments).

Estimated changes

Modified src/data/nat/basic.lean

deleted def nat.bit_cases

added theorem nat.bit_cases_on_bit0

added theorem nat.bit_cases_on_bit1

added theorem nat.bit_cases_on_bit

added theorem nat.bit_cases_on_inj

added theorem nat.bit_cases_on_injective