Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-25 03:10 d9083bcb

View on Github →

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

Estimated changes

modified theorem inv_lt_zero
deleted theorem inv_neg'
deleted theorem inv_pos'
modified theorem inv_pos
modified theorem hyperreal.omega_pos