feat(*): preparations for roots of unity (#4322)

Author: jcommelin

src/algebra/group_power/lemmas.lean

@@ -48,6 +48,15 @@ theorem list.sum_repeat : ∀ (a : A) (n : ℕ), (list.repeat a n).sum = n •
 @[simp, norm_cast] lemma units.coe_pow (u : units M) (n : ℕ) : ((u ^ n : units M) : M) = u ^ n :=
 (units.coe_hom M).map_pow u n
 
+lemma is_unit_of_pow_eq_one (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : 0 < n) :
+  is_unit x :=
+begin
+  cases n, { exact (nat.not_lt_zero _ hn).elim },
+  refine ⟨⟨x, x ^ n, _, _⟩, rfl⟩,
+  { rwa [pow_succ] at hx },
+  { rwa [pow_succ'] at hx }
+end
+
 end monoid
 
 theorem nat.nsmul_eq_mul (m n : ℕ) : m •ℕ n = m * n :=

src/data/int/gcd.lean

@@ -126,3 +126,14 @@ begin
 end
 
 end int
+
+lemma pow_gcd_eq_one {M : Type*} [monoid M] (x : M) {m n : ℕ} (hm : x ^ m = 1) (hn : x ^ n = 1) :
+  x ^ m.gcd n = 1 :=
+begin
+  cases m, { simp only [hn, nat.gcd_zero_left] },
+  obtain ⟨x, rfl⟩ : is_unit x,
+  { apply is_unit_of_pow_eq_one _ _ hm m.succ_pos },
+  simp only [← units.coe_pow] at *,
+  rw [← units.coe_one, ← gpow_coe_nat, ← units.ext_iff] at *,
+  simp only [nat.gcd_eq_gcd_ab, gpow_add, gpow_mul, hm, hn, one_gpow, one_mul]
+end

src/data/polynomial/ring_division.lean

@@ -348,17 +348,21 @@ calc ((roots ((X : polynomial R) ^ n - C a)).card : with_bot ℕ)
       ≤ degree ((X : polynomial R) ^ n - C a) : card_roots (X_pow_sub_C_ne_zero hn a)
   ... = n : degree_X_pow_sub_C hn a
 
+section nth_roots
 
 /-- `nth_roots n a` noncomputably returns the solutions to `x ^ n = a`-/
-def nth_roots {R : Type*} [integral_domain R] (n : ℕ) (a : R) : multiset R :=
+def nth_roots (n : ℕ) (a : R) : multiset R :=
 roots ((X : polynomial R) ^ n - C a)
 
-@[simp] lemma mem_nth_roots {R : Type*} [integral_domain R] {n : ℕ} (hn : 0 < n) {a x : R} :
+@[simp] lemma mem_nth_roots {n : ℕ} (hn : 0 < n) {a x : R} :
   x ∈ nth_roots n a ↔ x ^ n = a :=
 by rw [nth_roots, mem_roots (X_pow_sub_C_ne_zero hn a),
   is_root.def, eval_sub, eval_C, eval_pow, eval_X, sub_eq_zero_iff_eq]
 
-lemma card_nth_roots {R : Type*} [integral_domain R] (n : ℕ) (a : R) :
+@[simp] lemma nth_roots_zero (r : R) : nth_roots 0 r = 0 :=
+by simp only [empty_eq_zero, pow_zero, nth_roots, ← C_1, ← C_sub, roots_C]
+
+lemma card_nth_roots (n : ℕ) (a : R) :
   (nth_roots n a).card ≤ n :=
 if hn : n = 0
 then if h : (X : polynomial R) ^ n - C a = 0
@@ -369,6 +373,8 @@ then if h : (X : polynomial R) ^ n - C a = 0
 else by rw [← with_bot.coe_le_coe, ← degree_X_pow_sub_C (nat.pos_of_ne_zero hn) a];
   exact card_roots (X_pow_sub_C_ne_zero (nat.pos_of_ne_zero hn) a)
 
+end nth_roots
+
 lemma coeff_comp_degree_mul_degree (hqd0 : nat_degree q ≠ 0) :
   coeff (p.comp q) (nat_degree p * nat_degree q) =
   leading_coeff p * leading_coeff q ^ nat_degree p :=

src/group_theory/order_of_element.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl
 import algebra.big_operators.order
 import group_theory.coset
 import data.nat.totient
+import data.int.gcd
 import data.set.finite
 
 open function
@@ -271,12 +272,7 @@ open_locale classical
 
 lemma pow_gcd_card_eq_one_iff {n : ℕ} {a : α} :
   a ^ n = 1 ↔ a ^ (gcd n (fintype.card α)) = 1 :=
-⟨λ h, have hn : order_of a ∣ n, from dvd_of_mod_eq_zero $
-      by_contradiction (λ ha, by rw pow_eq_mod_order_of at h;
-        exact (not_le_of_gt (nat.mod_lt n (order_of_pos a)))
-          (order_of_le_of_pow_eq_one (nat.pos_of_ne_zero ha) h)),
-    let ⟨m, hm⟩ := dvd_gcd hn order_of_dvd_card_univ in
-    by rw [hm, pow_mul, pow_order_of_eq_one, one_pow],
+⟨λ h, pow_gcd_eq_one _ h $ pow_card_eq_one _,
   λ h, let ⟨m, hm⟩ := gcd_dvd_left n (fintype.card α) in
     by rw [hm, pow_mul, h, one_pow]⟩