basic): `simp` lemmas about inequalities with `bit*`
#2207

Merged

feat(data/nat/basic): `simp` lemmas about inequalities with `bit*` #2207

mergify merged 9 commits into master from bit-simp

feat(data/nat/basic): `simp` lemmas about inequalities with `bit*`

631b1700

urkud added awaiting-author

cipher1024 assigned

digama0 5 years ago

Fix compile of `computability/partrec_code`

9e699065

Fix `nat.bit_cases` to work for `Type*` too

8e47e4a7

Merge branch 'master' into bit-simp

a4753cc2

Generalize some lemmas to `linear_ordered_semiring`s

ed7cf0ef

urkud removed awaiting-author

urkud added awaiting-review

gebner commented on 2020-03-22

kim-em commented on 2020-03-22

kim-em removed awaiting-review

kim-em added awaiting-author

Apply suggestions from code review

754291d4

Apply suggestions from code review

d90e8ba8

urkud removed awaiting-author

urkud added awaiting-review

fixing a proof

6614e8cd

urkud removed awaiting-review

urkud added awaiting-author

sgouezel removed awaiting-author

sgouezel added ready-to-merge

sgouezel approved these changes on 2020-03-31

Merge branch 'master' into bit-simp

89de07cd

mergify merged cc20a865 into master 5 years ago

urkud deleted the bit-simp branch 5 years ago

Reviewers

sgouezel

kim-em

gebner

Assignees

digama0

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(data/nat/basic): `simp` lemmas about inequalities with `bit*` #2207 Merged

feat(data/nat/basic): `simp` lemmas about inequalities with `bit*` #2207

mathlib3
feat(data/nat/basic): `simp` lemmas about inequalities with `bit*`
#2207

Merged