chore(algebra/field_power): generalisation linter (#13107)

@alexjbest, this one is slightly more interesting, as the generalisation linter detected that two lemmas were stated incorrectly!




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/algebra/field_power.lean

@@ -37,14 +37,6 @@ open int
 
 variables {K : Type u} [linear_ordered_field K] {a : K} {n : ℤ}
 
-lemma zpow_eq_zero_iff (hn : 0 < n) :
-  a ^ n = 0 ↔ a = 0 :=
-begin
-  refine ⟨zpow_eq_zero, _⟩,
-  rintros rfl,
-  exact zero_zpow _ hn.ne'
-end
-
 lemma zpow_nonneg {a : K} (ha : 0 ≤ a) : ∀ (z : ℤ), 0 ≤ a ^ z
 | (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 _) }
@@ -96,14 +88,14 @@ calc p ^ z ≥ p ^ 0 : zpow_le_of_le hp hz
 theorem zpow_bit0_nonneg (a : K) (n : ℤ) : 0 ≤ a ^ bit0 n :=
 by { rw zpow_bit0₀, exact mul_self_nonneg _ }
 
-theorem zpow_two_nonneg (a : K) : 0 ≤ a ^ 2 :=
-pow_bit0_nonneg a 1
+theorem zpow_two_nonneg (a : K) : 0 ≤ a ^ (2 : ℤ) :=
+zpow_bit0_nonneg a 1
 
 theorem zpow_bit0_pos {a : K} (h : a ≠ 0) (n : ℤ) : 0 < a ^ bit0 n :=
 (zpow_bit0_nonneg a n).lt_of_ne (zpow_ne_zero _ h).symm
 
-theorem zpow_two_pos_of_ne_zero (a : K) (h : a ≠ 0) : 0 < a ^ 2 :=
-pow_bit0_pos h 1
+theorem zpow_two_pos_of_ne_zero (a : K) (h : a ≠ 0) : 0 < a ^ (2 : ℤ) :=
+zpow_bit0_pos h 1
 
 @[simp] theorem zpow_bit1_neg_iff : a ^ bit1 n < 0 ↔ a < 0 :=
 ⟨λ h, not_le.1 $ λ h', not_le.2 h $ zpow_nonneg h' _,
@@ -200,7 +192,7 @@ end
 end ordered
 
 section
-variables {K : Type*} [field K]
+variables {K : Type*} [division_ring K]
 
 @[simp, norm_cast] theorem rat.cast_zpow [char_zero K] (q : ℚ) (n : ℤ) :
   ((q ^ n : ℚ) : K) = q ^ n :=

src/algebra/group_with_zero/power.lean

@@ -217,6 +217,14 @@ by rw [zpow_bit1₀, (commute.refl a).mul_zpow₀]
 lemma zpow_eq_zero {x : G₀} {n : ℤ} (h : x ^ n = 0) : x = 0 :=
 classical.by_contradiction $ λ hx, zpow_ne_zero_of_ne_zero hx n h
 
+lemma zpow_eq_zero_iff {a : G₀} {n : ℤ} (hn : 0 < n) :
+  a ^ n = 0 ↔ a = 0 :=
+begin
+  refine ⟨zpow_eq_zero, _⟩,
+  rintros rfl,
+  exact zero_zpow _ hn.ne'
+end
+
 lemma zpow_ne_zero {x : G₀} (n : ℤ) : x ≠ 0 → x ^ n ≠ 0 :=
 mt zpow_eq_zero