Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-11 09:33 4e19dab9

View on Github →

chore(algebra/order/ring): Normalize _left/_right (#14985) Swap the left and right variants of

  • nonneg_of_mul_nonneg_
  • pos_of_mul_pos_
  • neg_of_mul_pos_
  • neg_of_mul_neg_

Estimated changes

modified theorem zero_lt.pos_of_mul_pos_left
modified theorem neg_of_mul_neg_left
modified theorem neg_of_mul_neg_right
modified theorem neg_of_mul_pos_left
modified theorem neg_of_mul_pos_right
modified theorem nonneg_of_mul_nonneg_left
modified theorem nonneg_of_mul_nonneg_right
modified theorem nonpos_of_mul_nonpos_left
modified theorem nonpos_of_mul_nonpos_right
modified theorem pos_of_mul_pos_left
modified theorem pos_of_mul_pos_right