feat(ring_theory/roots_of_unity): turn is_primitive_root into a mem…

…ber of `roots_of_unity` (#11739)

from flt-regular



Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

src/ring_theory/roots_of_unity.lean

@@ -229,6 +229,10 @@ structure is_primitive_root (ζ : M) (k : ℕ) : Prop :=
 (pow_eq_one : ζ ^ (k : ℕ) = 1)
 (dvd_of_pow_eq_one : ∀ l : ℕ, ζ ^ l = 1 → k ∣ l)
 
+/-- Turn a primitive root μ into a member of the `roots_of_unity` subgroup. -/
+@[simps] def is_primitive_root.to_roots_of_unity {μ : M} {n : ℕ+} (h : is_primitive_root μ n) :
+  roots_of_unity n M := roots_of_unity.mk_of_pow_eq μ h.pow_eq_one
+
 section primitive_roots
 variables {k : ℕ}