Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-26 13:30 1cf59fcc

View on Github →

chore(src/algebra/ordered_ring.lean): fix linting errors (#2827) Mentioned, but not really discussed, in this Zulip thread. This PR also removes mul_pos' and mul_nonneg' lemmas because they are now identical to the improved mul_pos and mul_nonneg.

Estimated changes

modified theorem four_pos
modified theorem gt_of_mul_lt_mul_neg_left
deleted theorem mul_nonneg'
modified theorem mul_nonneg
deleted theorem mul_pos'
modified theorem mul_pos
modified theorem mul_self_nonneg
modified theorem two_ge_one
modified theorem two_gt_one
modified theorem with_top.coe_eq_zero
modified theorem with_top.coe_zero
modified theorem with_top.top_ne_zero
modified theorem with_top.zero_eq_coe
modified theorem with_top.zero_ne_top