feat(number_theory/cyclotomic/basic): add is_primitive_root.adjoin (#…

…12716)

We add `is_cyclotomic_extension.is_primitive_root.adjoin`.

From flt-regular

src/number_theory/cyclotomic/basic.lean

@@ -278,6 +278,31 @@ begin
   exact ((iff_adjoin_eq_top {n} A B).mp h).2,
 end
 
+variable (A)
+
+lemma _root_.is_primitive_root.adjoin_is_cyclotomic_extension [is_domain B] {ζ : B} {n : ℕ+}
+  (h : is_primitive_root ζ n) : is_cyclotomic_extension {n} A (adjoin A ({ζ} : set B)) :=
+{ exists_root := λ i hi,
+  begin
+    rw [set.mem_singleton_iff] at hi,
+    refine ⟨⟨ζ, subset_adjoin $ set.mem_singleton ζ⟩, _⟩,
+    have := is_root_cyclotomic n.pos h,
+    rw [is_root.def, ← map_cyclotomic _ (algebra_map A B), eval_map, ← aeval_def, ← hi] at this,
+    rwa [← subalgebra.coe_eq_zero, aeval_subalgebra_coe, subtype.coe_mk]
+  end,
+  adjoin_roots := λ x,
+  begin
+    refine adjoin_induction' (λ b hb, _) (λ a, _) (λ b₁ b₂ hb₁ hb₂, _) (λ b₁ b₂ hb₁ hb₂, _) x,
+    { rw [set.mem_singleton_iff] at hb,
+      refine subset_adjoin _,
+      simp only [mem_singleton_iff, exists_eq_left, mem_set_of_eq, hb],
+      rw [← subalgebra.coe_eq_one, subalgebra.coe_pow, set_like.coe_mk],
+      exact ((is_primitive_root.iff_def ζ n).1 h).1 },
+    { exact subalgebra.algebra_map_mem _ _ },
+    { exact subalgebra.add_mem _ hb₁ hb₂ },
+    { exact subalgebra.mul_mem _ hb₁ hb₂ }
+  end }
+
 end
 
 section field

src/number_theory/cyclotomic/primitive_roots.lean

@@ -347,7 +347,7 @@ lemma norm_zeta_eq_one [is_cyclotomic_extension {n} K L] (hn : n ≠ 2)
   (hirr : irreducible (cyclotomic n K)) : norm K (zeta n K L) = 1 :=
 begin
   haveI := ne_zero.of_no_zero_smul_divisors K L n,
-  exact norm_eq_one (zeta_primitive_root n K L) hn hirr,
+  exact (zeta_primitive_root n K L).norm_eq_one hn hirr,
 end
 
 /-- If `is_prime_pow (n : ℕ)`, `n ≠ 2` and `irreducible (cyclotomic n K)` (in particular for
@@ -358,7 +358,7 @@ lemma is_prime_pow_norm_zeta_sub_one (hn : is_prime_pow (n : ℕ))
   norm K (zeta n K L - 1) = (n : ℕ).min_fac :=
 begin
   haveI := ne_zero.of_no_zero_smul_divisors K L n,
-  exact sub_one_norm_is_prime_pow (zeta_primitive_root n K L) hn hirr h,
+  exact (zeta_primitive_root n K L).sub_one_norm_is_prime_pow hn hirr h,
 end
 
 /-- If `irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is an odd
@@ -374,7 +374,7 @@ begin
   { refine ⟨λ hzero, _⟩,
     rw [pow_coe] at hzero,
     simpa [ne_zero.ne ((p : ℕ) : L)] using hzero },
-  exact sub_one_norm_prime_ne_two (zeta_primitive_root _ K L) hirr h,
+  exact (zeta_primitive_root _ K L).sub_one_norm_prime_ne_two hirr h,
 end
 
 /-- If `irreducible (cyclotomic p K)` (in particular for `K = ℚ`) and `p` is an odd prime,
@@ -384,7 +384,7 @@ lemma prime_ne_two_norm_zeta_sub_one {p : ℕ+} [ne_zero ((p : ℕ) : K)] [hpri
   norm K (zeta p K L - 1) = p :=
 begin
   haveI := ne_zero.of_no_zero_smul_divisors K L p,
-  exact sub_one_norm_prime (zeta_primitive_root _ K L) hirr h,
+  exact (zeta_primitive_root _ K L).sub_one_norm_prime hirr h,
 end
 
 /-- If `irreducible (cyclotomic (2 ^ k) K)` (in particular for `K = ℚ`) and `k` is at least `2`,