chore(algebra/{group_power,order}): split off field lemmas (#14849)

I want to refer to the rational numbers in the definition of a field, meaning we can't have `algebra.field.basic` in the transitive imports of `data.rat.basic`.

This is half of rearranging those imports: remove the definition of a field from the dependencies of basic lemmas about `nsmul`, `npow`, `zsmul` and `zpow`.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Author: Vierkantor

src/algebra/group_power/lemmas.lean

@@ -519,20 +519,6 @@ by simpa only [add_sub_cancel'_right] using one_add_mul_le_pow this n
 
 end linear_ordered_ring
 
-/-- Bernoulli's inequality reformulated to estimate `(n : K)`. -/
-theorem nat.cast_le_pow_sub_div_sub {K : Type*} [linear_ordered_field K] {a : K} (H : 1 < a)
-  (n : ℕ) :
-  (n : K) ≤ (a ^ n - 1) / (a - 1) :=
-(le_div_iff (sub_pos.2 H)).2 $ le_sub_left_of_add_le $
-  one_add_mul_sub_le_pow ((neg_le_self zero_le_one).trans H.le) _
-
-/-- For any `a > 1` and a natural `n` we have `n ≤ a ^ n / (a - 1)`. See also
-`nat.cast_le_pow_sub_div_sub` for a stronger inequality with `a ^ n - 1` in the numerator. -/
-theorem nat.cast_le_pow_div_sub {K : Type*} [linear_ordered_field K] {a : K} (H : 1 < a) (n : ℕ) :
-  (n : K) ≤ a ^ n / (a - 1) :=
-(n.cast_le_pow_sub_div_sub H).trans $ div_le_div_of_le (sub_nonneg.2 H.le)
-  (sub_le_self _ zero_le_one)
-
 namespace int
 
 alias int.units_sq ← int.units_pow_two

src/algebra/group_with_zero/power.lean

@@ -204,19 +204,3 @@ lemma monoid_with_zero_hom.map_zpow {G₀ G₀' : Type*} [group_with_zero G₀]
     rw [zpow_neg_succ_of_nat, zpow_neg_succ_of_nat],
     exact ((f.map_inv _).trans $ congr_arg _ $ f.to_monoid_hom.map_pow x _)
   end
-
--- I haven't been able to find a better home for this:
--- it belongs with other lemmas on `linear_ordered_field`, but
--- we need to wait until `zpow` has been defined in this file.
-section
-variables {R : Type*} [linear_ordered_field R] {a : R}
-
-lemma pow_minus_two_nonneg : 0 ≤ a^(-2 : ℤ) :=
-begin
-  simp only [inv_nonneg, zpow_neg],
-  change 0 ≤ a ^ ((2 : ℕ) : ℤ),
-  rw zpow_coe_nat,
-  apply sq_nonneg,
-end
-
-end

src/algebra/order/field_pow.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Scott Morrison
+-/
+import algebra.group_power.lemmas
+import data.nat.cast
+import algebra.group_with_zero.power
+import algebra.order.field
+/-!
+# Powers of elements of linear ordered fields
+
+Some results on integer powers of elements of a linear ordered field.
+These results are in their own file because they depend both on
+`linear_ordered_field` and on the API for `zpow`; neither should be obviously
+an ancestor of the other.
+-/
+
+section
+variables {R : Type*} [linear_ordered_field R] {a : R}
+
+lemma pow_minus_two_nonneg : 0 ≤ a^(-2 : ℤ) :=
+begin
+  simp only [inv_nonneg, zpow_neg],
+  change 0 ≤ a ^ ((2 : ℕ) : ℤ),
+  rw zpow_coe_nat,
+  apply sq_nonneg,
+end
+
+/-- Bernoulli's inequality reformulated to estimate `(n : K)`. -/
+theorem nat.cast_le_pow_sub_div_sub {K : Type*} [linear_ordered_field K] {a : K} (H : 1 < a)
+  (n : ℕ) :
+  (n : K) ≤ (a ^ n - 1) / (a - 1) :=
+(le_div_iff (sub_pos.2 H)).2 $ le_sub_left_of_add_le $
+  one_add_mul_sub_le_pow ((neg_le_self zero_le_one).trans H.le) _
+
+/-- For any `a > 1` and a natural `n` we have `n ≤ a ^ n / (a - 1)`. See also
+`nat.cast_le_pow_sub_div_sub` for a stronger inequality with `a ^ n - 1` in the numerator. -/
+theorem nat.cast_le_pow_div_sub {K : Type*} [linear_ordered_field K] {a : K} (H : 1 < a) (n : ℕ) :
+  (n : K) ≤ a ^ n / (a - 1) :=
+(n.cast_le_pow_sub_div_sub H).trans $ div_le_div_of_le (sub_nonneg.2 H.le)
+  (sub_le_self _ zero_le_one)
+
+end

src/analysis/special_functions/bernstein.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+import algebra.order.field_pow
 import ring_theory.polynomial.bernstein
 import topology.continuous_function.polynomial
 

src/analysis/specific_limits/normed.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker, Sébastien Gouëzel, Yury G. Kudryashov, Dylan MacKenzie, Patrick Massot
 -/
+import algebra.order.field_pow
 import analysis.asymptotics.asymptotics
 import analysis.specific_limits.basic