Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-15 05:41 931182ee

View on Github →

chore(algebra/ordered_ring): add a few simp lemmas (#5749)

  • fix misleading names neg_lt_iff_add_nonneg → neg_lt_iff_pos_add, neg_lt_iff_add_nonneg' → neg_lt_iff_pos_add';
  • add @[simp] to abs_mul_abs_self and abs_mul_self;
  • add lemmas neg_le_self_iff, neg_lt_self_iff, le_neg_self_iff, lt_neg_self_iff, abs_eq_self, abs_eq_neg_self.

Estimated changes

added theorem abs_eq_neg_self
added theorem abs_eq_self
modified theorem abs_mul_abs_self
modified theorem abs_mul_self
added theorem le_neg_self_iff
added theorem lt_neg_self_iff
added theorem neg_le_self_iff
added theorem neg_lt_self_iff
modified theorem neg_one_lt_zero