PR #2304 refactor(data/real/irrational): review

refactor(data/real/irrational): review #2304

mergify merged 5 commits into master from irrational

refactor(data/real/irrational): review

5e5ab76d

urkud added awaiting-review

jcommelin commented on 2020-04-01

sgouezel commented on 2020-04-01

Update src/data/real/irrational.lean

22bc9a0d

Update src/data/real/irrational.lean

f775753e

sgouezel removed awaiting-review

sgouezel added ready-to-merge

kim-em commented on 2020-04-01

Apply suggestions from code review

292e5bce

bryangingechen approved these changes on 2020-04-01

Merge branch 'master' into irrational

ad8b4155

mergify merged a8076b2c into master 5 years ago

mergify deleted the irrational branch 5 years ago

Reviewers

bryangingechen

kim-em

sgouezel

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone