chore(number_theory/cyclotomic/primitive_roots): generalisation linter (

#16013)

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

src/number_theory/cyclotomic/primitive_roots.lean

@@ -188,19 +188,22 @@ section norm
 
 namespace is_primitive_root
 
-variables [field L] {ζ : L} (hζ : is_primitive_root ζ n)
+section comm_ring
+
+variables [comm_ring L] {ζ : L} (hζ : is_primitive_root ζ n)
 variables {K} [field K] [algebra K L]
 
 /-- This mathematically trivial result is complementary to `norm_eq_one` below. -/
-lemma norm_eq_neg_one_pow (hζ : is_primitive_root ζ 2) : norm K ζ = (-1) ^ finrank K L :=
-by rw [hζ.eq_neg_one_of_two_right , show -1 = algebra_map K L (-1), by simp,
-  algebra.norm_algebra_map]
+lemma norm_eq_neg_one_pow (hζ : is_primitive_root ζ 2) [is_domain L] :
+  norm K ζ = (-1) ^ finrank K L :=
+by rw [hζ.eq_neg_one_of_two_right, show -1 = algebra_map K L (-1), by simp,
+       algebra.norm_algebra_map]
 
 include hζ
 
 /-- If `irreducible (cyclotomic n K)` (in particular for `K = ℚ`), the norm of a primitive root is
 `1` if `n ≠ 2`. -/
-lemma norm_eq_one [is_cyclotomic_extension {n} K L] (hn : n ≠ 2)
+lemma norm_eq_one [is_domain L] [is_cyclotomic_extension {n} K L] (hn : n ≠ 2)
   (hirr : irreducible (cyclotomic n K)) : norm K ζ = 1 :=
 begin
   haveI := is_cyclotomic_extension.ne_zero' n K L,
@@ -225,7 +228,7 @@ begin
   exact strict_mono.injective hodd.strict_mono_pow hz
 end
 
-lemma norm_of_cyclotomic_irreducible [is_cyclotomic_extension {n} K L]
+lemma norm_of_cyclotomic_irreducible [is_domain L] [is_cyclotomic_extension {n} K L]
   (hirr : irreducible (cyclotomic n K)) : norm K ζ = ite (n = 2) (-1) 1 :=
 begin
   split_ifs with hn,
@@ -236,6 +239,15 @@ begin
   { exact hζ.norm_eq_one hn hirr }
 end
 
+end comm_ring
+
+section field
+
+variables [field L] {ζ : L} (hζ : is_primitive_root ζ n)
+variables {K} [field K] [algebra K L]
+
+include hζ
+
 /-- If `irreducible (cyclotomic n K)` (in particular for `K = ℚ`), then the norm of
 `ζ - 1` is `eval 1 (cyclotomic n ℤ)`. -/
 lemma sub_one_norm_eq_eval_cyclotomic [is_cyclotomic_extension {n} K L]
@@ -458,6 +470,8 @@ begin
   { exact hζ.pow_sub_one_norm_prime_pow_ne_two hirr hs htwo }
 end
 
+end field
+
 end is_primitive_root
 
 namespace is_cyclotomic_extension