feat(algebra/order/ring): add odd_neg, odd_abs, generalize dvd/abs le…

…mmas (#9362)

src/algebra/order/ring.lean

@@ -1278,6 +1278,10 @@ begin
     mul_one, mul_neg_eq_neg_mul_symm, neg_add_rev, neg_neg],
 end
 
+end linear_ordered_comm_ring
+section
+variables [ring α] [linear_order α] {a b : α}
+
 @[simp] lemma abs_dvd (a b : α) : abs a ∣ b ↔ a ∣ b :=
 by { cases abs_choice a with h h; simp only [h, neg_dvd] }
 
@@ -1296,6 +1300,15 @@ lemma abs_dvd_abs (a b : α) : abs a ∣ abs b ↔ a ∣ b :=
 lemma even_abs {a : α} : even (abs a) ↔ even a :=
 dvd_abs _ _
 
+lemma odd_abs {a : α} : odd (abs a) ↔ odd a :=
+by { cases abs_choice a with h h; simp only [h, odd_neg] }
+
+end
+
+section linear_ordered_comm_ring
+
+variables [linear_ordered_comm_ring α]
+
 /-- Pullback a `linear_ordered_comm_ring` under an injective map.
 See note [reducible non-instances]. -/
 @[reducible]

src/algebra/ring/basic.lean

@@ -841,6 +841,17 @@ end
 @[simp] theorem even_neg (a : α) : even (-a) ↔ even a :=
 dvd_neg _ _
 
+lemma odd.neg {a : α} (hp : odd a) : odd (-a) :=
+begin
+  obtain ⟨k, hk⟩ := hp,
+  use -(k + 1),
+  rw [mul_neg_eq_neg_mul_symm, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add,
+    neg_add_cancel_right, ←neg_add, hk],
+end
+
+@[simp] lemma odd_neg (a : α) : odd (-a) ↔ odd a :=
+⟨λ h, neg_neg a ▸ h.neg, odd.neg⟩
+
 end ring
 
 section comm_ring