mathlib

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

chore(algebra/ordered_field): merge `inv_pos` / `zero_lt_inv` with `inv_pos'` / `inv_neg` (#2226) * chore(algebra/ordered_field): merge `inv_pos` / `zero_lt_inv` with `inv_pos'` / `inv_neg` Also move some lemmas to `linear_ordered_field` * Update src/data/real/hyperreal.lean * Fix compile * Actually fix compile of `data/real/hyperreal` Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>