From 702cfc1746560d103ba5e2d6854de1b14c0855f3 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 29 Oct 2021 18:05:37 +0100
Subject: [PATCH 1/2] feat(algebra/group_power/lemmas): remove commutativity
 requirement from `is_unit_pos_pow_iff`

Also adds a simp lemma, is_unit_pow_succ_iff
---
 src/algebra/group_power/lemmas.lean | 23 ++++++++++++++---------
 1 file changed, 14 insertions(+), 9 deletions(-)

diff --git a/src/algebra/group_power/lemmas.lean b/src/algebra/group_power/lemmas.lean
index 47cf14ed799d3..760b934c109c7 100644
--- a/src/algebra/group_power/lemmas.lean
+++ b/src/algebra/group_power/lemmas.lean
@@ -49,17 +49,22 @@ lemma inv_of_pow (m : M) [invertible m] (n : ℕ) [invertible (m ^ n)] :
 lemma is_unit.pow {m : M} (n : ℕ) : is_unit m → is_unit (m ^ n) :=
 λ ⟨u, hu⟩, ⟨u ^ n, by simp *⟩
 
-lemma is_unit_pos_pow_iff {M : Type*} [comm_monoid M] {m : M} {n : ℕ} (h : 0 < n) :
-  is_unit (m ^ n) ↔ is_unit m :=
+@[simp] lemma is_unit_pow_succ_iff {m : M} {n : ℕ} : is_unit (m ^ n.succ) ↔ is_unit m :=
 begin
-  obtain ⟨p, rfl⟩ := nat.exists_eq_succ_of_ne_zero h.ne',
   refine ⟨λ h, _, is_unit.pow _⟩,
-  obtain ⟨⟨k, k', hk, hk'⟩, h⟩ := h,
-  rw [units.coe_mk] at h,
-  refine ⟨⟨m, m ^ p * k', _, _⟩, _⟩,
-  { rw [←mul_assoc, ←pow_succ, ←h, hk] },
-  { rw [mul_right_comm, ←pow_succ', ←h, hk] },
-  { exact units.coe_mk _ _ _ _ }
+  obtain ⟨u, hu⟩ := h,
+  have h_comm : ↑u⁻¹ * m ^ n = m ^ n * ↑u⁻¹,
+  { rw [units.inv_mul_eq_iff_eq_mul, ←mul_assoc, units.eq_mul_inv_iff_mul_eq, hu, ←pow_add,
+        ←pow_add, add_comm], },
+  refine ⟨⟨m, ↑u⁻¹ * m ^ n, _, _⟩, rfl⟩,
+  { rw [h_comm, ←mul_assoc, ←pow_succ, ←hu, units.mul_inv], },
+  { rw [mul_assoc, ←pow_succ', ←hu, units.inv_mul], },
+end
+
+lemma is_unit_pos_pow_iff {m : M} {n : ℕ} (h : 0 < n) : is_unit (m ^ n) ↔ is_unit m :=
+begin
+  obtain ⟨p, rfl⟩ := nat.exists_eq_succ_of_ne_zero h.ne',
+  exact is_unit_pow_succ_iff,
 end
 
 /-- If `x ^ n.succ = 1` then `x` has an inverse, `x^n`. -/

From 510adc4923fb82bab9c27e44f9cf377a39961116 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 29 Oct 2021 18:08:31 +0100
Subject: [PATCH 2/2] Update lemmas.lean

---
 src/algebra/group_power/lemmas.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/algebra/group_power/lemmas.lean b/src/algebra/group_power/lemmas.lean
index 760b934c109c7..97ea39b995572 100644
--- a/src/algebra/group_power/lemmas.lean
+++ b/src/algebra/group_power/lemmas.lean
@@ -67,6 +67,9 @@ begin
   exact is_unit_pow_succ_iff,
 end
 
+lemma is_unit_mul_self_iff {m : M} : is_unit (m * m) ↔ is_unit m :=
+by rw [←pow_two, is_unit_pow_succ_iff]
+
 /-- If `x ^ n.succ = 1` then `x` has an inverse, `x^n`. -/
 def invertible_of_pow_succ_eq_one (x : M) (n : ℕ) (hx : x ^ n.succ = 1) :
   invertible x :=