move(algebra/field_power): Put lemmas in the correct place (#16465)

`algebra.field_power` is only made of lemmas that belong elsewhere. Move them and delete the file.

Golf proofs while we're at it and make `min_le_of_zpow_le_max` an iff.

src/algebra/field/basic.lean

@@ -94,6 +94,18 @@ class division_ring (K : Type u) extends ring K, div_inv_monoid K, nontrivial K,
 (qsmul : ℚ → K → K := qsmul_rec rat_cast)
 (qsmul_eq_mul' : ∀ (a : ℚ) (x : K), qsmul a x = rat_cast a * x . try_refl_tac)
 
+@[priority 100] -- see Note [lower instance priority]
+instance division_ring.to_division_semiring [division_ring α] : division_semiring α :=
+{ ..‹division_ring α›, ..(infer_instance : semiring α) }
+
+section division_ring
+variables [division_ring α]
+
+@[simp] lemma zpow_bit1_neg (x : α) (n : ℤ) : (-x) ^ bit1 n = - x ^ bit1 n :=
+by rw [zpow_bit1', zpow_bit1', neg_mul_neg, neg_mul_eq_mul_neg]
+
+end division_ring
+
 /-- A `semifield` is a `comm_semiring` with multiplicative inverses for nonzero elements. -/
 @[protect_proj, ancestor comm_semiring division_semiring comm_group_with_zero]
 class semifield (α : Type*) extends comm_semiring α, division_semiring α, comm_group_with_zero α
@@ -111,10 +123,6 @@ See also Note [forgetful inheritance].
 @[protect_proj, ancestor comm_ring div_inv_monoid nontrivial]
 class field (K : Type u) extends comm_ring K, division_ring K
 
-@[priority 100] -- see Note [lower instance priority]
-instance division_ring.to_division_semiring [division_ring α] : division_semiring α :=
-{ ..‹division_ring α›, ..(infer_instance : semiring α) }
-
 section division_semiring
 variables [division_semiring α] {a b c : α}
 

src/algebra/group_power/order.lean

@@ -222,23 +222,6 @@ begin
       by { rw [pow_succ _ n], exact mul_le_mul_of_nonneg_left (ih (nat.succ_ne_zero k)) h2 }
 end
 
-theorem pow_lt_pow_of_lt_left (Hxy : x < y) (Hxpos : 0 ≤ x) (Hnpos : 0 < n) :
-  x ^ n < y ^ n :=
-begin
-  cases lt_or_eq_of_le Hxpos,
-  { rw ← tsub_add_cancel_of_le (nat.succ_le_of_lt Hnpos),
-    induction (n - 1), { simpa only [pow_one] },
-    rw [pow_add, pow_add, nat.succ_eq_add_one, pow_one, pow_one],
-    apply mul_lt_mul ih (le_of_lt Hxy) h (le_of_lt (pow_pos (lt_trans h Hxy) _)) },
-  { rw [←h, zero_pow Hnpos], apply pow_pos (by rwa ←h at Hxy : 0 < y),}
-end
-
-lemma pow_lt_one (h₀ : 0 ≤ a) (h₁ : a < 1) {n : ℕ} (hn : n ≠ 0) : a ^ n < 1 :=
-(one_pow n).subst (pow_lt_pow_of_lt_left h₁ h₀ (nat.pos_of_ne_zero hn))
-
-theorem strict_mono_on_pow (hn : 0 < n) : strict_mono_on (λ x : R, x ^ n) (set.Ici 0) :=
-λ x hx y hy h, pow_lt_pow_of_lt_left h hx hn
-
 theorem one_le_pow_of_one_le (H : 1 ≤ a) : ∀ (n : ℕ), 1 ≤ a ^ n
 | 0     := by rw [pow_zero]
 | (n+1) := by { rw pow_succ, simpa only [mul_one] using mul_le_mul H (one_le_pow_of_one_le n)
@@ -283,13 +266,24 @@ lemma pow_lt_pow_of_lt_one (h : 0 < a) (ha : a < 1) {i j : ℕ} (hij : i < j) :
 | (k+1) := by { rw [pow_succ, pow_succ],
     exact mul_le_mul hab (pow_le_pow_of_le_left _) (pow_nonneg ha _) (le_trans ha hab) }
 
+lemma pow_lt_pow_of_lt_left (h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, 0 < n → x ^ n < y ^ n
+| 0 hn := hn.false.elim
+| (n + 1) _ := by simpa only [pow_succ'] using
+    mul_lt_mul' (pow_le_pow_of_le_left hx h.le _) h hx (pow_pos (hx.trans_lt h) _)
+
+lemma pow_lt_one (h₀ : 0 ≤ a) (h₁ : a < 1) {n : ℕ} (hn : n ≠ 0) : a ^ n < 1 :=
+(one_pow n).subst (pow_lt_pow_of_lt_left h₁ h₀ (nat.pos_of_ne_zero hn))
+
 lemma one_lt_pow (ha : 1 < a) {n : ℕ} (hn : n ≠ 0) : 1 < a ^ n :=
 pow_zero a ▸ pow_lt_pow ha (pos_iff_ne_zero.2 hn)
 
 lemma pow_le_one : ∀ (n : ℕ) (h₀ : 0 ≤ a) (h₁ : a ≤ 1), a ^ n ≤ 1
 | 0       h₀ h₁ := (pow_zero a).le
 | (n + 1) h₀ h₁ := (pow_succ' a n).le.trans (mul_le_one (pow_le_one n h₀ h₁) h₀ h₁)
 
+lemma strict_mono_on_pow (hn : 0 < n) : strict_mono_on (λ x : R, x ^ n) (set.Ici 0) :=
+λ x hx y hy h, pow_lt_pow_of_lt_left h hx hn
+
 lemma sq_pos_of_pos (ha : 0 < a) : 0 < a ^ 2 := by { rw sq, exact mul_pos ha ha }
 
 end ordered_semiring

src/algebra/order/archimedean.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import algebra.field_power
 import data.int.least_greatest
 import data.rat.floor
 

src/algebra/order/field.lean

@@ -22,7 +22,7 @@ A linear ordered (semi)field is a (semi)field equipped with a linear order such
 
 set_option old_structure_cmd true
 
-open order_dual
+open function order_dual
 
 variables {α β : Type*}
 
@@ -66,7 +66,7 @@ def injective.linear_ordered_field [linear_ordered_field α] [has_zero β] [has_
 end function
 
 section linear_ordered_semifield
-variables [linear_ordered_semifield α] {a b c d e : α}
+variables [linear_ordered_semifield α] {a b c d e : α} {m n : ℤ}
 
 /-- `equiv.mul_left₀` as an order_iso. -/
 @[simps {simp_rhs := tt}]
@@ -124,6 +124,14 @@ by { rw div_eq_mul_inv, exact mul_nonpos_of_nonpos_of_nonneg ha (inv_nonneg.2 hb
 lemma div_nonpos_of_nonneg_of_nonpos (ha : 0 ≤ a) (hb : b ≤ 0) : a / b ≤ 0 :=
 by { rw div_eq_mul_inv, exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb) }
 
+lemma zpow_nonneg (ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n
+| (n : ℕ) := by { rw zpow_coe_nat, exact pow_nonneg ha _ }
+| -[1+n]  := by { rw zpow_neg_succ_of_nat, exact inv_nonneg.2 (pow_nonneg ha _) }
+
+lemma zpow_pos_of_pos (ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n
+| (n : ℕ) := by { rw zpow_coe_nat, exact pow_pos ha _ }
+| -[1+n]  := by { rw zpow_neg_succ_of_nat, exact inv_pos.2 (pow_pos ha _) }
+
 /-!
 ### Relating one division with another term.
 -/
@@ -417,6 +425,72 @@ by rwa [lt_one_div (@zero_lt_one α _ _) h1, one_div_one]
 lemma one_le_one_div (h1 : 0 < a) (h2 : a ≤ 1) : 1 ≤ 1 / a :=
 by rwa [le_one_div (@zero_lt_one α _ _) h1, one_div_one]
 
+/-! ### Integer powers -/
+
+lemma zpow_le_of_le (ha : 1 ≤ a) (h : m ≤ n) : a ^ m ≤ a ^ n :=
+begin
+  have ha₀ : 0 < a, from one_pos.trans_le ha,
+  lift n - m to ℕ using sub_nonneg.2 h with k hk,
+  calc a ^ m = a ^ m * 1 : (mul_one _).symm
+  ... ≤ a ^ m * a ^ k : mul_le_mul_of_nonneg_left (one_le_pow_of_one_le ha _) (zpow_nonneg ha₀.le _)
+  ... = a ^ n : by rw [← zpow_coe_nat, ← zpow_add₀ ha₀.ne', hk, add_sub_cancel'_right]
+end
+
+lemma zpow_le_one_of_nonpos (ha : 1 ≤ a) (hn : n ≤ 0) : a ^ n ≤ 1 :=
+(zpow_le_of_le ha hn).trans_eq $ zpow_zero _
+
+lemma one_le_zpow_of_nonneg (ha : 1 ≤ a) (hn : 0 ≤ n) : 1 ≤ a ^ n :=
+(zpow_zero _).symm.trans_le $ zpow_le_of_le ha hn
+
+protected lemma nat.zpow_pos_of_pos {a : ℕ} (h : 0 < a) (n : ℤ) : 0 < (a : α)^n :=
+by { apply zpow_pos_of_pos, exact_mod_cast h }
+
+lemma nat.zpow_ne_zero_of_pos {a : ℕ} (h : 0 < a) (n : ℤ) : (a : α)^n ≠ 0 :=
+(nat.zpow_pos_of_pos h n).ne'
+
+lemma one_lt_zpow (ha : 1 < a) : ∀ n : ℤ, 0 < n → 1 < a ^ n
+| (n : ℕ) h := (zpow_coe_nat _ _).symm.subst (one_lt_pow ha $ int.coe_nat_ne_zero.mp h.ne')
+| -[1+ n] h := ((int.neg_succ_not_pos _).mp h).elim
+
+lemma zpow_strict_mono (hx : 1 < a) : strict_mono ((^) a : ℤ → α) :=
+strict_mono_int_of_lt_succ $ λ n,
+have xpos : 0 < a, from zero_lt_one.trans hx,
+calc a ^ n < a ^ n * a : lt_mul_of_one_lt_right (zpow_pos_of_pos xpos _) hx
+... = a ^ (n + 1) : (zpow_add_one₀ xpos.ne' _).symm
+
+lemma zpow_strict_anti (h₀ : 0 < a) (h₁ : a < 1) : strict_anti ((^) a : ℤ → α) :=
+strict_anti_int_of_succ_lt $ λ n,
+calc a ^ (n + 1) = a ^ n * a : zpow_add_one₀ h₀.ne' _
+... < a ^ n * 1 : (mul_lt_mul_left $ zpow_pos_of_pos h₀ _).2 h₁
+... = a ^ n : mul_one _
+
+@[simp] lemma zpow_lt_iff_lt (hx : 1 < a) : a ^ m < a ^ n ↔ m < n := (zpow_strict_mono hx).lt_iff_lt
+@[simp] lemma zpow_le_iff_le (hx : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n := (zpow_strict_mono hx).le_iff_le
+
+@[simp] lemma div_pow_le (ha : 0 ≤ a) (hb : 1 ≤ b) (k : ℕ) : a/b^k ≤ a :=
+div_le_self ha $ one_le_pow_of_one_le hb _
+
+lemma zpow_injective (h₀ : 0 < a) (h₁ : a ≠ 1) : injective ((^) a : ℤ → α) :=
+begin
+  rcases h₁.lt_or_lt with H|H,
+  { exact (zpow_strict_anti h₀ H).injective },
+  { exact (zpow_strict_mono H).injective }
+end
+
+@[simp] lemma zpow_inj (h₀ : 0 < a) (h₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n :=
+(zpow_injective h₀ h₁).eq_iff
+
+lemma zpow_le_max_of_min_le {x : α} (hx : 1 ≤ x) {a b c : ℤ} (h : min a b ≤ c) :
+  x ^ -c ≤ max (x ^ -a) (x ^ -b) :=
+begin
+  have : antitone (λ n : ℤ, x ^ -n) := λ m n h, zpow_le_of_le hx (neg_le_neg h),
+  exact (this h).trans_eq this.map_min,
+end
+
+lemma zpow_le_max_iff_min_le {x : α} (hx : 1 < x) {a b c : ℤ} :
+  x ^ -c ≤ max (x ^ -a) (x ^ -b) ↔ min a b ≤ c :=
+by simp_rw [le_max_iff, min_le_iff, zpow_le_iff_le hx, neg_le_neg_iff]
+
 /-!
 ### Results about halving.
 
@@ -564,7 +638,7 @@ by simpa [mul_comm] using hs.mul_left ha
 end linear_ordered_semifield
 
 section
-variables [linear_ordered_field α] {a b c d : α}
+variables [linear_ordered_field α] {a b c d : α} {n : ℤ}
 
 /-! ### Lemmas about pos, nonneg, nonpos, neg -/
 
@@ -589,6 +663,29 @@ div_neg_iff.2 $ or.inr ⟨ha, hb⟩
 lemma div_neg_of_pos_of_neg (ha : 0 < a) (hb : b < 0) : a / b < 0 :=
 div_neg_iff.2 $ or.inl ⟨ha, hb⟩
 
+lemma zpow_bit0_nonneg (a : α) (n : ℤ) : 0 ≤ a ^ bit0 n :=
+(mul_self_nonneg _).trans_eq $ (zpow_bit0 _ _).symm
+
+lemma zpow_two_nonneg (a : α) : 0 ≤ a ^ (2 : ℤ) := zpow_bit0_nonneg _ _
+
+lemma zpow_bit0_pos (h : a ≠ 0) (n : ℤ) : 0 < a ^ bit0 n :=
+(zpow_bit0_nonneg a n).lt_of_ne (zpow_ne_zero _ h).symm
+
+lemma zpow_two_pos_of_ne_zero (h : a ≠ 0) : 0 < a ^ (2 : ℤ) := zpow_bit0_pos h _
+
+@[simp] lemma zpow_bit1_neg_iff : a ^ bit1 n < 0 ↔ a < 0 :=
+⟨λ h, not_le.1 $ λ h', not_le.2 h $ zpow_nonneg h' _,
+ λ h, by rw [bit1, zpow_add_one₀ h.ne]; exact mul_neg_of_pos_of_neg (zpow_bit0_pos h.ne _) h⟩
+
+@[simp] lemma zpow_bit1_nonneg_iff : 0 ≤ a ^ bit1 n ↔ 0 ≤ a :=
+le_iff_le_iff_lt_iff_lt.2 zpow_bit1_neg_iff
+
+@[simp] lemma zpow_bit1_nonpos_iff : a ^ bit1 n ≤ 0 ↔ a ≤ 0 :=
+by rw [le_iff_lt_or_eq, le_iff_lt_or_eq, zpow_bit1_neg_iff, zpow_eq_zero_iff (int.bit1_ne_zero n)]
+
+@[simp] lemma zpow_bit1_pos_iff : 0 < a ^ bit1 n ↔ 0 < a :=
+lt_iff_lt_of_le_iff_le zpow_bit1_nonpos_iff
+
 /-! ### Relating one division with another term -/
 
 lemma div_le_iff_of_neg (hc : c < 0) : b / c ≤ a ↔ a * c ≤ b :=

src/algebra/order/positive/field.lean

@@ -3,8 +3,8 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import algebra.order.field
 import algebra.order.positive.ring
-import algebra.field_power
 
 /-!
 # Algebraic structures on the set of positive numbers