fix(library/algebra/ordered_filed): rename theorems

library/algebra/ordered_field.lean

@@ -434,37 +434,37 @@ section discrete_linear_ordered_field
       absurd Hl' (ne_of_lt Hl)),
     lt_of_le_of_ne H1 Hn
 
-  theorem div_lt_div_of_lt (Ha : 0 < a) (H : a < b) : 1 / b < 1 / a :=
+  theorem one_div_lt_one_div_of_lt (Ha : 0 < a) (H : a < b) : 1 / b < 1 / a :=
     lt_of_not_ge
       (assume H',
       absurd H (not_lt_of_ge (le_of_one_div_le_one_div Ha H')))
 
-  theorem div_le_div_of_le (Ha : 0 < a) (H : a ≤ b) : 1 / b ≤ 1 / a :=
+  theorem one_div_le_one_div_of_le (Ha : 0 < a) (H : a ≤ b) : 1 / b ≤ 1 / a :=
     le_of_not_gt
       (assume H',
       absurd H (not_le_of_gt (lt_of_one_div_lt_one_div Ha H')))
 
-  theorem div_lt_div_of_lt_neg (Hb : b < 0) (H : a < b) : 1 / b < 1 / a :=
+  theorem one_div_lt_one_div_of_lt_of_neg (Hb : b < 0) (H : a < b) : 1 / b < 1 / a :=
     lt_of_not_ge
       (assume H',
       absurd H (not_lt_of_ge (le_of_one_div_le_one_div_of_neg Hb H')))
 
-  theorem div_le_div_of_le_neg (Hb : b < 0) (H : a ≤ b) : 1 / b ≤ 1 / a :=
+  theorem one_div_le_one_div_of_le_of_neg (Hb : b < 0) (H : a ≤ b) : 1 / b ≤ 1 / a :=
     le_of_not_gt
       (assume H',
       absurd H (not_le_of_gt (lt_of_one_div_lt_one_div_of_neg Hb H')))
 
   theorem one_lt_one_div (H1 : 0 < a) (H2 : a < 1) : 1 < 1 / a :=
-    one_div_one ▸ div_lt_div_of_lt H1 H2
+    one_div_one ▸ one_div_lt_one_div_of_lt H1 H2
 
   theorem one_le_one_div (H1 : 0 < a) (H2 : a ≤ 1) : 1 ≤ 1 / a :=
-    one_div_one ▸ div_le_div_of_le H1 H2
+    one_div_one ▸ one_div_le_one_div_of_le H1 H2
 
   theorem one_div_lt_neg_one (H1 : a < 0) (H2 : -1 < a) : 1 / a < -1 :=
-    one_div_neg_one_eq_neg_one ▸ div_lt_div_of_lt_neg H1 H2
+    one_div_neg_one_eq_neg_one ▸ one_div_lt_one_div_of_lt_of_neg H1 H2
 
   theorem one_div_le_neg_one (H1 : a < 0) (H2 : -1 ≤ a) : 1 / a ≤ -1 :=
-    one_div_neg_one_eq_neg_one ▸ div_le_div_of_le_neg H1 H2
+    one_div_neg_one_eq_neg_one ▸ one_div_le_one_div_of_le_of_neg H1 H2
 
   theorem div_lt_div_of_pos_of_lt_of_pos (Hb : 0 < b) (H : b < a) (Hc : 0 < c) : c / a < c / b :=
     begin
@@ -473,7 +473,7 @@ section discrete_linear_ordered_field
       apply mul_neg_of_pos_of_neg,
       exact Hc,
       apply iff.mpr !sub_neg_iff_lt,
-      apply div_lt_div_of_lt,
+      apply one_div_lt_one_div_of_lt,
       repeat assumption
     end
 

library/data/pnat.lean

@@ -116,7 +116,7 @@ theorem inv_pos (n : ℕ+) : n⁻¹ > 0 := one_div_pos_of_pos !rat_of_pnat_is_po
 theorem inv_le_one (n : ℕ+) : n⁻¹ ≤ (1 : ℚ) :=
   begin
     rewrite [↑inv, -one_div_one],
-    apply div_le_div_of_le,
+    apply one_div_le_one_div_of_le,
     apply rat.zero_lt_one,
     apply rat_of_pnat_ge_one
   end
@@ -124,7 +124,7 @@ theorem inv_le_one (n : ℕ+) : n⁻¹ ≤ (1 : ℚ) :=
 theorem inv_lt_one_of_gt {n : ℕ+} (H : n~ > 1) : n⁻¹ < (1 : ℚ) :=
   begin
     rewrite [↑inv, -one_div_one],
-    apply div_lt_div_of_lt,
+    apply one_div_lt_one_div_of_lt,
     apply rat.zero_lt_one,
     rewrite pnat.to_rat_of_nat,
     apply (of_nat_lt_of_nat_of_lt H)
@@ -158,7 +158,7 @@ theorem one_lt_two : pone < 2 := !nat.le.refl
 theorem inv_two_mul_lt_inv (n : ℕ+) : (2 * n)⁻¹ < n⁻¹ :=
   begin
     rewrite ↑inv,
-    apply div_lt_div_of_lt,
+    apply one_div_lt_one_div_of_lt,
     apply rat_of_pnat_is_pos,
     have H : n~ < (2 * n)~, begin
       rewrite -one_mul at {1},
@@ -172,10 +172,10 @@ theorem inv_two_mul_lt_inv (n : ℕ+) : (2 * n)⁻¹ < n⁻¹ :=
 theorem inv_two_mul_le_inv (n : ℕ+) : (2 * n)⁻¹ ≤ n⁻¹ := rat.le_of_lt !inv_two_mul_lt_inv
 
 theorem inv_ge_of_le {p q : ℕ+} (H : p ≤ q) : q⁻¹ ≤ p⁻¹ :=
-  div_le_div_of_le !rat_of_pnat_is_pos (rat_of_pnat_le_of_pnat_le H)
+  one_div_le_one_div_of_le !rat_of_pnat_is_pos (rat_of_pnat_le_of_pnat_le H)
 
 theorem inv_gt_of_lt {p q : ℕ+} (H : p < q) : q⁻¹ < p⁻¹ :=
-  div_lt_div_of_lt !rat_of_pnat_is_pos (rat_of_pnat_lt_of_pnat_lt H)
+  one_div_lt_one_div_of_lt !rat_of_pnat_is_pos (rat_of_pnat_lt_of_pnat_lt H)
 
 theorem ge_of_inv_le {p q : ℕ+} (H : p⁻¹ ≤ q⁻¹) : q ≤ p :=
   pnat_le_of_rat_of_pnat_le (le_of_one_div_le_one_div !rat_of_pnat_is_pos H)
@@ -274,10 +274,10 @@ theorem pnat_cancel' (n m : ℕ+) : (n * n * m)⁻¹ * (rat_of_pnat n * rat_of_p
 definition pceil (a : ℚ) : ℕ+ := tag (ubound a) !ubound_pos
 
 theorem pceil_helper {a : ℚ} {n : ℕ+} (H : pceil a ≤ n) (Ha : a > 0) : n⁻¹ ≤ 1 / a :=
-  rat.le.trans (inv_ge_of_le H) (div_le_div_of_le Ha (ubound_ge a))
+  rat.le.trans (inv_ge_of_le H) (one_div_le_one_div_of_le Ha (ubound_ge a))
 
 theorem inv_pceil_div (a b : ℚ) (Ha : a > 0) (Hb : b > 0) : (pceil (a / b))⁻¹ ≤ b / a :=
-  !one_div_one_div ▸ div_le_div_of_le
+  !one_div_one_div ▸ one_div_le_one_div_of_le
     (one_div_pos_of_pos (div_pos_of_pos_of_pos Hb Ha))
     (!div_div_eq_mul_div⁻¹ ▸ !rat.one_mul⁻¹ ▸ !ubound_ge)
 

library/data/real/complete.lean

@@ -509,7 +509,7 @@ have H₁ : succ n ≥ ceil (2 / ε), from of_int_le_of_int_of_le this,
 have H₂ : succ n ≥ 2 / ε, from !le.trans !le_ceil H₁,
 have H₃ : 2 / ε > 0, from div_pos_of_pos_of_pos two_pos H,
 have 1 / succ n < ε, from calc
-  1 / succ n ≤ 1 / (2 / ε) : div_le_div_of_le H₃ H₂
+  1 / succ n ≤ 1 / (2 / ε) : one_div_le_one_div_of_le H₃ H₂
     ... = ε / 2       : one_div_div
     ... < ε           : div_two_lt_of_pos H,
 exists.intro n this
@@ -832,7 +832,7 @@ theorem over_seq_mono (i j : ℕ) (H : i ≤ j) : over_seq j ≤ over_seq i :=
   end
 
 theorem rat_power_two_inv_ge (k : ℕ+) : 1 / rat.pow 2 k~ ≤ k⁻¹ :=
-  rat.div_le_div_of_le !rat_of_pnat_is_pos !rat_power_two_le
+  rat.one_div_le_one_div_of_le !rat_of_pnat_is_pos !rat_power_two_le
 
 open rat_seq
 theorem regular_lemma_helper {s : seq} {m n : ℕ+} (Hm : m ≤ n)