fix(number_theory/cyclotomic/basic): change variable names, fix doc (#…

…16901)

The docstring of `is_cyclotomic` was using `a ∈ S` and `n` (`∈ S`) interchangeably. I've switched to `n` uniformly, because I think `a` risks being confused as a term of the ring `A`.

src/number_theory/cyclotomic/basic.lean

@@ -72,20 +72,20 @@ variables [field K] [field L] [algebra K L]
 noncomputable theory
 
 /-- Given an `A`-algebra `B` and `S : set ℕ+`, we define `is_cyclotomic_extension S A B` requiring
-that there is a `a`-th primitive root of unity in `B` for all `a ∈ S` and that `B` is generated
+that there is a `n`-th primitive root of unity in `B` for all `n ∈ S` and that `B` is generated
 over `A` by the roots of `X ^ n - 1`. -/
 @[mk_iff] class is_cyclotomic_extension : Prop :=
-(exists_prim_root {a : ℕ+} (ha : a ∈ S) : ∃ r : B, is_primitive_root r a)
-(adjoin_roots : ∀ (x : B), x ∈ adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 })
+(exists_prim_root {n : ℕ+} (ha : n ∈ S) : ∃ r : B, is_primitive_root r n)
+(adjoin_roots : ∀ (x : B), x ∈ adjoin A { b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1 })
 
 namespace is_cyclotomic_extension
 
 section basic
 
 /-- A reformulation of `is_cyclotomic_extension` that uses `⊤`. -/
 lemma iff_adjoin_eq_top : is_cyclotomic_extension S A B ↔
- (∀ (a : ℕ+), a ∈ S → ∃ r : B, is_primitive_root r a) ∧
- (adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 } = ⊤) :=
+ (∀ (n : ℕ+), n ∈ S → ∃ r : B, is_primitive_root r n) ∧
+ (adjoin A { b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1 } = ⊤) :=
 ⟨λ h, ⟨λ _, h.exists_prim_root, algebra.eq_top_iff.2 h.adjoin_roots⟩,
   λ h, ⟨h.1, algebra.eq_top_iff.1 h.2⟩⟩