mathlib3
931182ee - chore(algebra/ordered_ring): add a few simp lemmas (#5749)

Commit
5 years ago
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`.
Author
Parents
Loading