feat(algebra/ordered_group, algebra/ordered_ring): add some lemmas ab…

…out abs (#7612)

src/algebra/ordered_group.lean

@@ -731,6 +731,8 @@ lemma le_iff_forall_pos_lt_add : a ≤ b ↔ ∀ ε, 0 < ε → a < b + ε :=
 /-- `abs a` is the absolute value of `a`. -/
 def abs (a : α) : α := max a (-a)
 
+lemma abs_choice (x : α) : abs x = x ∨ abs x = -x := max_choice _ _
+
 lemma abs_of_nonneg (h : 0 ≤ a) : abs a = a :=
 max_eq_left $ (neg_nonpos.2 h).trans h
 
@@ -841,14 +843,22 @@ calc abs a = abs (a - b + b)     : by rw [sub_add_cancel]
 lemma abs_abs_sub_abs_le_abs_sub (a b : α) : abs (abs a - abs b) ≤ abs (a - b) :=
 abs_sub_le_iff.2 ⟨abs_sub_abs_le_abs_sub _ _, by rw abs_sub; apply abs_sub_abs_le_abs_sub⟩
 
+lemma eq_or_eq_neg_of_abs_eq (h : abs a = b) : a = b ∨ a = -b :=
+by simpa only [← h, eq_comm, eq_neg_iff_eq_neg] using abs_choice a
+
 lemma abs_eq (hb : 0 ≤ b) : abs a = b ↔ a = b ∨ a = -b :=
-iff.intro
-  begin
-    cases le_total a 0 with a_nonpos a_nonneg,
-    { rw [abs_of_nonpos a_nonpos, neg_eq_iff_neg_eq, eq_comm], exact or.inr },
-    { rw [abs_of_nonneg a_nonneg, eq_comm], exact or.inl }
-  end
-  (by intro h; cases h; subst h; try { rw abs_neg }; exact abs_of_nonneg hb)
+begin
+  refine ⟨eq_or_eq_neg_of_abs_eq, _⟩,
+  rintro (rfl|rfl); simp only [abs_neg, abs_of_nonneg hb]
+end
+
+lemma abs_eq_abs : abs a = abs b ↔ a = b ∨ a = -b :=
+begin
+  refine ⟨λ h, _, λ h, _⟩,
+  { obtain rfl | rfl := eq_or_eq_neg_of_abs_eq h;
+    simpa only [neg_eq_iff_neg_eq, neg_inj, or.comm, @eq_comm _ (-b)] using abs_choice b },
+  { cases h; simp only [h, abs_neg] },
+end
 
 lemma abs_le_max_abs_abs (hab : a ≤ b)  (hbc : b ≤ c) : abs b ≤ max (abs a) (abs c) :=
 abs_le'.2

src/algebra/ordered_ring.lean

@@ -1161,6 +1161,24 @@ begin
     mul_one, mul_neg_eq_neg_mul_symm, neg_add_rev, neg_neg],
 end
 
+@[simp] lemma abs_dvd (a b : α) : abs a ∣ b ↔ a ∣ b :=
+by { cases abs_choice a with h h; simp only [h, neg_dvd] }
+
+lemma abs_dvd_self (a : α) : abs a ∣ a :=
+(abs_dvd a a).mpr (dvd_refl a)
+
+@[simp] lemma dvd_abs (a b : α) : a ∣ abs b ↔ a ∣ b :=
+by { cases abs_choice b with h h; simp only [h, dvd_neg] }
+
+lemma self_dvd_abs (a : α) : a ∣ abs a :=
+(dvd_abs a a).mpr (dvd_refl a)
+
+lemma abs_dvd_abs (a b : α) : abs a ∣ abs b ↔ a ∣ b :=
+(abs_dvd _ _).trans (dvd_abs _ _)
+
+lemma even_abs {a : α} : even (abs a) ↔ even a :=
+dvd_abs _ _
+
 /-- Pullback a `linear_ordered_comm_ring` under an injective map. -/
 def function.injective.linear_ordered_comm_ring {β : Type*}
   [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [nontrivial β]