From 8a67cf51f3370b875fc190393ba53f9ed71908e2 Mon Sep 17 00:00:00 2001 From: Eric Rodriguez Date: Mon, 31 Jan 2022 07:25:05 +0000 Subject: [PATCH] feat(ring_theory/roots_of_unity): turn `is_primitive_root` into a member 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 | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/ring_theory/roots_of_unity.lean b/src/ring_theory/roots_of_unity.lean index abde3b7271c4f..fc69b54141245 100644 --- a/src/ring_theory/roots_of_unity.lean +++ b/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 : ℕ}