feat(library/algebra/*,library/data/*): small additions and changes

library/algebra/ordered_field.lean

@@ -521,7 +521,7 @@ section discrete_linear_ordered_field
     ge_sub_of_abs_sub_le_left (!abs_sub ▸ H)
 
   theorem abs_sub_square : abs (a - b) * abs (a - b) = a * a + b * b - 2 * a * b :=
-    by rewrite [abs_mul_self, *mul_sub_left_distrib, *mul_sub_right_distrib,
+    by rewrite [abs_mul_abs_self, *mul_sub_left_distrib, *mul_sub_right_distrib,
              sub_add_eq_sub_sub, sub_neg_eq_add, *right_distrib, sub_add_eq_sub_sub, *one_mul,
              *add.assoc, {_ + b * b}add.comm, {_ + (b * b + _)}add.comm, mul.comm b a, *add.assoc]
 
@@ -529,7 +529,7 @@ section discrete_linear_ordered_field
   begin
     apply nonneg_le_nonneg_of_squares_le,
     repeat apply abs_nonneg,
-    rewrite [*abs_sub_square, *abs_abs, *abs_mul_self],
+    rewrite [*abs_sub_square, *abs_abs, *abs_mul_abs_self],
     apply sub_le_sub_left,
     rewrite *mul.assoc,
     apply mul_le_mul_of_nonneg_left,

library/algebra/ordered_ring.lean

@@ -642,8 +642,11 @@ section
                     ... = abs a * -b    : by rewrite (abs_of_nonpos H1)
                     ... = abs a * abs b : by rewrite (abs_of_nonpos H2)))
 
-  theorem abs_mul_self (a : A) : abs a * abs a = a * a :=
+  theorem abs_mul_abs_self (a : A) : abs a * abs a = a * a :=
   abs.by_cases rfl !neg_mul_neg
+
+  theorem abs_mul_self (a : A) : abs (a * a) = a * a :=
+  by rewrite [abs_mul, abs_mul_abs_self]
 end
 
 /- TODO: Multiplication and one, starting with mult_right_le_one_le. -/

library/data/nat/parity.lean

@@ -217,6 +217,18 @@ by_contradiction (suppose ¬ odd (n*m),
   assert even (n*m), from even_of_not_odd this,
   absurd `even (n * m + n)` (not_even_of_odd (odd_add_of_even_of_odd this `odd n`)))
 
+lemma even_of_even_mul_self {n} : even (n * n) → even n :=
+suppose even (n * n),
+by_contradiction (suppose odd n,
+  have odd (n * n), from odd_mul_of_odd_of_odd this this,
+  show false, from this `even (n * n)`)
+
+lemma odd_of_odd_mul_self {n} : odd (n * n) → odd n :=
+suppose odd (n * n),
+  suppose even n,
+  have even (n * n), from !even_mul_of_even_left this,
+  show false, from `odd (n * n)` this
+
 lemma eq_of_div2_of_even {n m : nat} : n div 2 = m div 2 → (even n ↔ even m) → n = m :=
 assume h₁ h₂,
  or.elim (em (even n))

library/data/rat/basic.lean

@@ -543,7 +543,7 @@ theorem eq_num_div_denom (a : ℚ) : a = num a / denom a :=
 have H : of_int (denom a) ≠ 0, from assume H', ne_of_gt (denom_pos a) (of_int.inj H'),
 iff.mpr (eq_div_iff_mul_eq H) (mul_denom a)
 
-theorem of_nat_div {a b : ℤ} (H : b ∣ a) : of_int (a div b) = of_int a / of_int b :=
+theorem of_int_div {a b : ℤ} (H : b ∣ a) : of_int (a div b) = of_int a / of_int b :=
 decidable.by_cases
   (assume bz : b = 0,
     by rewrite [bz, div_zero, int.div_zero])