feat: Prove r_one_zpow (#20338)

ldct · ldct · commit e92b32904d55 · 2024-12-31T12:20:47.000Z
Prove `DihedralGroup.r_one_zpow`, which extends `r_one_pow` to the integers.
diff --git a/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean b/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
@@ -90,6 +90,14 @@ theorem sr_mul_r (i j : ZMod n) : sr i * r j = sr (i + j) :=
 theorem sr_mul_sr (i j : ZMod n) : sr i * sr j = r (j - i) :=
   rfl
 
+@[simp]
+theorem inv_r (i : ZMod n) : (r i)⁻¹ = r (-i) :=
+  rfl
+
+@[simp]
+theorem inv_sr (i : ZMod n) : (sr i)⁻¹ = sr i :=
+  rfl
+
 theorem one_def : (1 : DihedralGroup n) = r 0 :=
   rfl
 
@@ -134,6 +142,10 @@ theorem r_one_pow (k : ℕ) : (r 1 : DihedralGroup n) ^ k = r k := by
     norm_cast
     rw [Nat.one_add]
 
+@[simp]
+theorem r_one_zpow (k : ℤ) : (r 1 : DihedralGroup n) ^ k = r k := by
+  cases k <;> simp
+
 -- @[simp] -- Porting note: simp changes the goal to `r 0 = 1`. `r_one_pow_n` is no longer useful.
 theorem r_one_pow_n : r (1 : ZMod n) ^ n = 1 := by
   rw [r_one_pow, one_def]
