feat(RingTheory/RootsOfUnity/Basic): add more covenient version of a lemma (#13375)

This provides
```lean
lemma eq_pow_of_mem_rootsOfUnity' {k : ℕ} (hk : 0 < k) {ζ : R} (hζ : IsPrimitiveRoot ζ k) {ξ : Rˣ}
    (hξ : ξ ∈ rootsOfUnity (⟨k, hk⟩ : ℕ+) R) : ∃ i < k, ζ ^ i = ξ
```
for ease of use compared with [IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/RootsOfUnity/Basic.html#IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity), which requires `k` to be a `PNat` and `ζ` to be a unit.

Author: MichaelStollBayreuth

Mathlib/RingTheory/RootsOfUnity/Basic.lean

@@ -834,6 +834,16 @@ theorem eq_pow_of_mem_rootsOfUnity {k : ℕ+} {ζ ξ : Rˣ} (h : IsPrimitiveRoot
       mul_one]
 #align is_primitive_root.eq_pow_of_mem_roots_of_unity IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity
 
+/-- A version of `IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity` that takes a natural number `k`
+as argument instead of a `PNat` (and `ζ : R` instead of `ζ : Rˣ`). -/
+lemma eq_pow_of_mem_rootsOfUnity' {k : ℕ} (hk : 0 < k) {ζ : R} (hζ : IsPrimitiveRoot ζ k) {ξ : Rˣ}
+    (hξ : ξ ∈ rootsOfUnity (⟨k, hk⟩ : ℕ+) R) :
+    ∃ i < k, ζ ^ i = ξ := by
+  have hζ' : IsPrimitiveRoot (hζ.isUnit hk).unit (⟨k, hk⟩ : ℕ+) := isUnit_unit hk hζ
+  obtain ⟨i, hi₁, hi₂⟩ := hζ'.eq_pow_of_mem_rootsOfUnity hξ
+  simpa only [Units.val_pow_eq_pow_val, IsUnit.unit_spec]
+    using ⟨i, hi₁, congrArg ((↑) : Rˣ → R) hi₂⟩
+
 theorem eq_pow_of_pow_eq_one {k : ℕ} {ζ ξ : R} (h : IsPrimitiveRoot ζ k) (hξ : ξ ^ k = 1)
     (h0 : 0 < k) : ∃ i < k, ζ ^ i = ξ := by
   lift ζ to Rˣ using h.isUnit h0