`inv_neg`
#2226

Merged

chore(algebra/ordered_field): merge `inv_pos` / `zero_lt_inv` with `inv_pos'` / `inv_neg` #2226

mergify merged 6 commits into master from inv-pos

chore(algebra/ordered_field): merge `inv_pos` / `zero_lt_inv` with `i…

6c2c3045

kim-em commented on 2020-03-24

Update src/data/real/hyperreal.lean

3dcaf3d2

kim-em approved these changes on 2020-03-24

Fix compile

82fa7378

sgouezel added ready-to-merge

Actually fix compile of `data/real/hyperreal`

bd735084

Merge branch 'master' into inv-pos

4b07562d

Merge branch 'master' into inv-pos

e231b0a0

mergify merged d9083bcb into master 6 years ago

urkud deleted the inv-pos branch 6 years ago

Reviewers

kim-em

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone