refactor(algebra/group_power/lemmas): assume n ≠ 0 instead of 0 < n (#17323)

Also rename `is_unit_pos_pow_iff` to `is_unit_pow_iff`.

Author: urkud

src/algebra/associated.lean

@@ -177,7 +177,7 @@ begin
   intro h,
   obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_lt hn,
   rw [pow_succ, add_comm] at h,
-  exact (or_iff_left_of_imp ((is_unit_pos_pow_iff (nat.succ_pos _)).mp)).mp (of_irreducible_mul h)
+  exact (or_iff_left_of_imp is_unit_pow_succ_iff.mp).mp (of_irreducible_mul h)
 end
 
 theorem irreducible_or_factor {α} [monoid α] (x : α) (h : ¬ is_unit x) :

src/algebra/group_power/lemmas.lean

@@ -56,8 +56,9 @@ begin
   exact and.left
 end
 
-lemma is_unit_pos_pow_iff {m : M} :
-  ∀ {n : ℕ} (h : 0 < n), is_unit (m ^ n) ↔ is_unit m
+lemma is_unit_pow_iff {m : M} :
+  ∀ {n : ℕ} (h : n ≠ 0), is_unit (m ^ n) ↔ is_unit m
+| 0 h := (h rfl).elim
 | (n + 1) _ := is_unit_pow_succ_iff
 
 /-- If `x ^ n.succ = 1` then `x` has an inverse, `x^n`. -/
@@ -66,15 +67,15 @@ def invertible_of_pow_succ_eq_one (x : M) (n : ℕ) (hx : x ^ n.succ = 1) :
 ⟨x ^ n, (pow_succ' x n).symm.trans hx, (pow_succ x n).symm.trans hx⟩
 
 /-- If `x ^ n = 1` then `x` has an inverse, `x^(n - 1)`. -/
-def invertible_of_pow_eq_one (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : 0 < n) :
+def invertible_of_pow_eq_one (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : n ≠ 0) :
   invertible x :=
 begin
   apply invertible_of_pow_succ_eq_one x (n - 1),
   convert hx,
-  exact tsub_add_cancel_of_le (nat.succ_le_of_lt hn),
+  exact nat.succ_pred_eq_of_pos (pos_iff_ne_zero.2 hn),
 end
 
-lemma is_unit_of_pow_eq_one (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : 0 < n) :
+lemma is_unit_of_pow_eq_one (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : n ≠ 0) :
   is_unit x :=
 begin
   haveI := invertible_of_pow_eq_one x n hx hn,

src/algebra/is_prime_pow.lean

@@ -43,7 +43,7 @@ lemma not_is_prime_pow_one : ¬ is_prime_pow (1 : R) :=
 begin
   simp only [is_prime_pow_def, not_exists, not_and', and_imp],
   intros x n hn hx ht,
-  exact ht.not_unit (is_unit_of_pow_eq_one x n hx hn),
+  exact ht.not_unit (is_unit_of_pow_eq_one x n hx hn.ne'),
 end
 
 lemma prime.is_prime_pow {p : R} (hp : prime p) : is_prime_pow p :=

src/data/int/gcd.lean

@@ -384,8 +384,7 @@ lemma pow_gcd_eq_one {M : Type*} [monoid M] (x : M) {m n : ℕ} (hm : x ^ m = 1)
   x ^ m.gcd n = 1 :=
 begin
   cases m, { simp only [hn, nat.gcd_zero_left] },
-  obtain ⟨x, rfl⟩ : is_unit x,
-  { apply is_unit_of_pow_eq_one _ _ hm m.succ_pos },
+  lift x to Mˣ using is_unit_of_pow_eq_one _ _ hm m.succ_ne_zero,
   simp only [← units.coe_pow] at *,
   rw [← units.coe_one, ← zpow_coe_nat, ← units.ext_iff] at *,
   simp only [nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, hm, hn, one_zpow, one_mul]

src/data/polynomial/unit_trinomial.lean

@@ -190,7 +190,7 @@ begin
   { have key : ∀ k ∈ p.support, (p.coeff k) ^ 2 = 1 :=
     λ k hk, int.sq_eq_one_of_sq_le_three ((single_le_sum
       (λ k hk, sq_nonneg (p.coeff k)) hk).trans hp.le) (mem_support_iff.mp hk),
-    refine is_unit_trinomial_iff.mpr ⟨_, λ k hk, is_unit_of_pow_eq_one _ 2 (key k hk) zero_lt_two⟩,
+    refine is_unit_trinomial_iff.mpr ⟨_, λ k hk, is_unit_of_pow_eq_one _ 2 (key k hk) two_ne_zero⟩,
     rw [sum_def, sum_congr rfl key, sum_const, nat.smul_one_eq_coe] at hp,
     exact nat.cast_injective hp },
 end

src/field_theory/abel_ruffini.lean

@@ -107,7 +107,7 @@ begin
   have key : ∀ σ : (X ^ n - 1 : F[X]).gal, ∃ m : ℕ, σ a = a ^ m,
   { intro σ,
     obtain ⟨m, hm⟩ := map_root_of_unity_eq_pow_self σ.to_alg_hom
-      ⟨is_unit.unit (is_unit_of_pow_eq_one a n ha hn'),
+      ⟨is_unit.unit (is_unit_of_pow_eq_one a n ha hn),
       by { ext, rwa [units.coe_pow, is_unit.unit_spec, subtype.coe_mk n hn'] }⟩,
     use m,
     convert hm },

src/linear_algebra/matrix/zpow.lean

@@ -123,12 +123,11 @@ lemma is_unit_det_zpow_iff {A : M} {z : ℤ} :
 begin
   induction z using int.induction_on with z IH z IH,
   { simp },
-  { rw [←int.coe_nat_succ, zpow_coe_nat, det_pow, is_unit_pos_pow_iff (z.zero_lt_succ),
-        ←int.coe_nat_zero, int.coe_nat_eq_coe_nat_iff],
-    simp },
-  { rw [←neg_add', ←int.coe_nat_succ, zpow_neg_coe_nat, is_unit_nonsing_inv_det_iff,
-        det_pow, is_unit_pos_pow_iff (z.zero_lt_succ), neg_eq_zero, ←int.coe_nat_zero,
+  { rw [←int.coe_nat_succ, zpow_coe_nat, det_pow, is_unit_pow_succ_iff, ←int.coe_nat_zero,
         int.coe_nat_eq_coe_nat_iff],
+    simp },
+  { rw [←neg_add', ←int.coe_nat_succ, zpow_neg_coe_nat, is_unit_nonsing_inv_det_iff, det_pow,
+        is_unit_pow_succ_iff, neg_eq_zero, ←int.coe_nat_zero, int.coe_nat_eq_coe_nat_iff],
     simp }
 end
 

src/ring_theory/roots_of_unity.lean

@@ -134,7 +134,7 @@ let h : ∀ ξ : roots_of_unity n R, (σ ξ) ^ (n : ℕ) = 1 := λ ξ, by
 { change (σ (ξ : Rˣ)) ^ (n : ℕ) = 1,
   rw [←map_pow, ←units.coe_pow, show ((ξ : Rˣ) ^ (n : ℕ) = 1), from ξ.2,
       units.coe_one, map_one σ] } in
-{ to_fun := λ ξ, ⟨@unit_of_invertible _ _ _ (invertible_of_pow_eq_one _ _ (h ξ) n.2),
+{ to_fun := λ ξ, ⟨@unit_of_invertible _ _ _ (invertible_of_pow_eq_one _ _ (h ξ) n.ne_zero),
     by { ext, rw units.coe_pow, exact h ξ }⟩,
   map_one' := by { ext, exact map_one σ },
   map_mul' := λ ξ₁ ξ₂, by { ext, rw [subgroup.coe_mul, units.coe_mul], exact map_mul σ _ _ } }
@@ -710,9 +710,9 @@ lemma eq_pow_of_pow_eq_one {k : ℕ} {ζ ξ : R}
   (h : is_primitive_root ζ k) (hξ : ξ ^ k = 1) (h0 : 0 < k) :
   ∃ i < k, ζ ^ i = ξ :=
 begin
-  obtain ⟨ζ, rfl⟩ := h.is_unit h0,
-  obtain ⟨ξ, rfl⟩ := is_unit_of_pow_eq_one ξ k hξ h0,
-  obtain ⟨k, rfl⟩ : ∃ k' : ℕ+, k = k' := ⟨⟨k, h0⟩, rfl⟩,
+  lift ζ to Rˣ using h.is_unit h0,
+  lift ξ to Rˣ using is_unit_of_pow_eq_one ξ k hξ h0.ne',
+  lift k to ℕ+ using h0,
   simp only [← units.coe_pow, ← units.ext_iff],
   rw coe_units_iff at h,
   apply h.eq_pow_of_mem_roots_of_unity,