Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-05 11:03 b1920f59

View on Github →

chore(algebra/ordered_field): add simp attributes to inv_pos' and others (#1400)

Estimated changes

modified theorem inv_neg'
modified theorem inv_nonneg
modified theorem inv_nonpos
modified theorem inv_pos'