chore: refactor roots of unity to avoid PNat (#18516)

This is an attempt to refactor the definition of `rootsOfUnity` using a `Nat` instead of a `PNat`.

* In the definition of `rootsOfUnity`, we replace `(n : ℕ+)` by `(n : ℕ)`. The definition does not require `n` to be nonzero; it gives that `rootsOfUnity 0 M` is the top subgroup of the unit group of `M`.
* For results that need a positive `n`, we replace `(n : ℕ+)` with `(n : ℕ) [NeZero n]` in the parameters. In this way, they transparently apply when a `PNat` is used for `n` since `n` gets coerced to `Nat` and an `NeZero (n : ℕ)` instance is available.

The main benefit is that one no longer needs constructions like `rootsOfUnity ⟨n, <proof that n is positive⟩) R` when `n` is a natural number; one can simply use `rootsOfUnity n R`. (One may need to turn the positivity proof into an `NeZero` instance, however, if that is not available automatically.)

In addition, the code in `Mathlib.RingTheory.RootsOfUnity.Basic` can be simplified a bit in places, e.g., `x ^ (k : ℕ)` can be replaced by `x ^ k` and `∃ (i : ℕ), i < k ∧ P i` can be replaced by `∃ i < k, P i`. One result (`eq_pow_of_mem_rootsOfUnity'`; it was translating between `Nat`s and `PNat`s) can be removed altogether.

Since I was going through this file anyway, I took the opportunity to replace `=>` by `↦` and to do some golfing as well.

What this PR does *not* do is also refactoring cyclotomic extensions to not use (sets of) `PNat`s. This is a more complex matter and requires more thought and discussion.

Author: MichaelStollBayreuth

Mathlib/FieldTheory/KummerExtension.lean

@@ -246,7 +246,7 @@ We first develop the theory for a specific `K[n√a] := AdjoinRoot (X ^ n - C a)
 The main result is the description of the galois group: `autAdjoinRootXPowSubCEquiv`.
 -/
 
-variable {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) (hn : 0 < n)
+variable {n : ℕ} (hζ : (primitiveRoots n K).Nonempty)
 variable (a : K) (H : Irreducible (X ^ n - C a))
 
 set_option quotPrecheck false in
@@ -280,14 +280,15 @@ theorem Polynomial.separable_X_pow_sub_C_of_irreducible : (X ^ n - C a).Separabl
   exact (hζ.map_of_injective (algebraMap K K[n√a]).injective).injOn_pow_mul
     (root_X_pow_sub_C_ne_zero (lt_of_le_of_ne (show 1 ≤ n from hn) (Ne.symm hn')) _)
 
+variable (n)
+
 /-- The natural embedding of the roots of unity of `K` into `Gal(K[ⁿ√a]/K)`, by sending
 `η ↦ (ⁿ√a ↦ η • ⁿ√a)`. Also see `autAdjoinRootXPowSubC` for the `AlgEquiv` version. -/
 noncomputable
 def autAdjoinRootXPowSubCHom :
-    rootsOfUnity ⟨n, hn⟩ K →* (K[n√a] →ₐ[K] K[n√a]) where
+    rootsOfUnity n K →* (K[n√a] →ₐ[K] K[n√a]) where
   toFun := fun η ↦ liftHom (X ^ n - C a) (((η : Kˣ) : K) • (root _) : K[n√a]) <| by
     have := (mem_rootsOfUnity' _ _).mp η.prop
-    dsimp at this
     rw [map_sub, map_pow, aeval_C, aeval_X, Algebra.smul_def, mul_pow, root_X_pow_sub_C_pow,
       AdjoinRoot.algebraMap_eq, ← map_pow, this, map_one, one_mul, sub_self]
   map_one' := algHom_ext <| by simp
@@ -298,11 +299,13 @@ def autAdjoinRootXPowSubCHom :
 See `autAdjoinRootXPowSubCEquiv`. -/
 noncomputable
 def autAdjoinRootXPowSubC :
-    rootsOfUnity ⟨n, hn⟩ K →* (K[n√a] ≃ₐ[K] K[n√a]) :=
-  (AlgEquiv.algHomUnitsEquiv _ _).toMonoidHom.comp (autAdjoinRootXPowSubCHom hn a).toHomUnits
+    rootsOfUnity n K →* (K[n√a] ≃ₐ[K] K[n√a]) :=
+  (AlgEquiv.algHomUnitsEquiv _ _).toMonoidHom.comp (autAdjoinRootXPowSubCHom n a).toHomUnits
+
+variable {n}
 
 lemma autAdjoinRootXPowSubC_root (η) :
-    autAdjoinRootXPowSubC hn a η (root _) = ((η : Kˣ) : K) • root _ := by
+    autAdjoinRootXPowSubC n a η (root _) = ((η : Kˣ) : K) • root _ := by
   dsimp [autAdjoinRootXPowSubC, autAdjoinRootXPowSubCHom, AlgEquiv.algHomUnitsEquiv]
   apply liftHom_root
 
@@ -311,34 +314,33 @@ variable {a}
 /-- The inverse function of `autAdjoinRootXPowSubC` if `K` has all roots of unity.
 See `autAdjoinRootXPowSubCEquiv`. -/
 noncomputable
-def AdjoinRootXPowSubCEquivToRootsOfUnity (σ : K[n√a] ≃ₐ[K] K[n√a]) :
-    rootsOfUnity ⟨n, hn⟩ K :=
+def AdjoinRootXPowSubCEquivToRootsOfUnity [NeZero n] (σ : K[n√a] ≃ₐ[K] K[n√a]) :
+    rootsOfUnity n K :=
   letI := Fact.mk H
   letI : IsDomain K[n√a] := inferInstance
   letI := Classical.decEq K
-  (rootsOfUnityEquivOfPrimitiveRoots (n := ⟨n, hn⟩) (algebraMap K K[n√a]).injective hζ).symm
+  (rootsOfUnityEquivOfPrimitiveRoots (n := n) (algebraMap K K[n√a]).injective hζ).symm
     (rootsOfUnity.mkOfPowEq (if a = 0 then 1 else σ (root _) / root _) (by
     -- The if is needed in case `n = 1` and `a = 0` and `K[n√a] = K`.
     split
     · exact one_pow _
     rw [div_pow, ← map_pow]
-    simp only [PNat.mk_coe, root_X_pow_sub_C_pow, ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]
+    simp only [root_X_pow_sub_C_pow, ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]
     rw [div_self]
     rwa [Ne, map_eq_zero_iff _ (algebraMap K _).injective]))
 
 /-- The equivalence between the roots of unity of `K` and `Gal(K[ⁿ√a]/K)`. -/
 noncomputable
-def autAdjoinRootXPowSubCEquiv :
-    rootsOfUnity ⟨n, hn⟩ K ≃* (K[n√a] ≃ₐ[K] K[n√a]) where
-  __ := autAdjoinRootXPowSubC hn a
-  invFun := AdjoinRootXPowSubCEquivToRootsOfUnity hζ hn H
+def autAdjoinRootXPowSubCEquiv [NeZero n] :
+    rootsOfUnity n K ≃* (K[n√a] ≃ₐ[K] K[n√a]) where
+  __ := autAdjoinRootXPowSubC n a
+  invFun := AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
   left_inv := by
     intro η
     have := Fact.mk H
     have : IsDomain K[n√a] := inferInstance
     letI : Algebra K K[n√a] := inferInstance
-    apply (rootsOfUnityEquivOfPrimitiveRoots
-      (n := ⟨n, hn⟩) (algebraMap K K[n√a]).injective hζ).injective
+    apply (rootsOfUnityEquivOfPrimitiveRoots (algebraMap K K[n√a]).injective hζ).injective
     ext
     simp only [AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
       autAdjoinRootXPowSubC_root, Algebra.smul_def, ne_eq, MulEquiv.apply_symm_apply,
@@ -347,36 +349,34 @@ def autAdjoinRootXPowSubCEquiv :
     split_ifs with h
     · obtain rfl := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) h
       have : (η : Kˣ) = 1 := (pow_one _).symm.trans η.prop
-      simp only [PNat.mk_one, this, Units.val_one, map_one]
-    · exact mul_div_cancel_right₀ _ (root_X_pow_sub_C_ne_zero' hn h)
+      simp only [this, Units.val_one, map_one]
+    · exact mul_div_cancel_right₀ _ (root_X_pow_sub_C_ne_zero' (NeZero.pos n) h)
   right_inv := by
     intro e
     have := Fact.mk H
     letI : Algebra K K[n√a] := inferInstance
     apply AlgEquiv.coe_algHom_injective
     apply AdjoinRoot.algHom_ext
-    simp only [AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
-      AlgHom.coe_coe, autAdjoinRootXPowSubC_root, Algebra.smul_def, PNat.mk_coe,
-      AdjoinRootXPowSubCEquivToRootsOfUnity]
+    simp only [AdjoinRootXPowSubCEquivToRootsOfUnity, AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe,
+      MonoidHom.toOneHom_coe, AlgHom.coe_coe, autAdjoinRootXPowSubC_root, Algebra.smul_def]
     rw [rootsOfUnityEquivOfPrimitiveRoots_symm_apply, rootsOfUnity.val_mkOfPowEq_coe]
     split_ifs with h
     · obtain rfl := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) h
       rw [(pow_one _).symm.trans (root_X_pow_sub_C_pow 1 a), one_mul,
         ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]
-    · refine div_mul_cancel₀ _ (root_X_pow_sub_C_ne_zero' hn h)
+    · refine div_mul_cancel₀ _ (root_X_pow_sub_C_ne_zero' (NeZero.pos n) h)
 
-lemma autAdjoinRootXPowSubCEquiv_root (η) :
-    autAdjoinRootXPowSubCEquiv hζ hn H η (root _) = ((η : Kˣ) : K) • root _ :=
-  autAdjoinRootXPowSubC_root hn a η
+lemma autAdjoinRootXPowSubCEquiv_root [NeZero n] (η) :
+    autAdjoinRootXPowSubCEquiv hζ H η (root _) = ((η : Kˣ) : K) • root _ :=
+  autAdjoinRootXPowSubC_root a η
 
-lemma autAdjoinRootXPowSubCEquiv_symm_smul (σ) :
-    ((autAdjoinRootXPowSubCEquiv hζ hn H).symm σ : Kˣ) • (root _ : K[n√a]) = σ (root _) := by
+lemma autAdjoinRootXPowSubCEquiv_symm_smul [NeZero n] (σ) :
+    ((autAdjoinRootXPowSubCEquiv hζ H).symm σ : Kˣ) • (root _ : K[n√a]) = σ (root _) := by
   have := Fact.mk H
   simp only [autAdjoinRootXPowSubCEquiv, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
     MulEquiv.symm_mk, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, AdjoinRootXPowSubCEquivToRootsOfUnity,
-    AdjoinRoot.algebraMap_eq, Units.smul_def, Algebra.smul_def,
-    rootsOfUnityEquivOfPrimitiveRoots_symm_apply, rootsOfUnity.mkOfPowEq, PNat.mk_coe,
-    Units.val_ofPowEqOne, ite_mul, one_mul, ne_eq]
+    AdjoinRoot.algebraMap_eq, rootsOfUnity.mkOfPowEq, Units.smul_def, Algebra.smul_def,
+    rootsOfUnityEquivOfPrimitiveRoots_symm_apply, Units.val_ofPowEqOne, ite_mul, one_mul]
   simp_rw [← root_X_pow_sub_C_eq_zero_iff H]
   split_ifs with h
   · rw [h, map_zero]
@@ -459,8 +459,8 @@ abbrev rootOfSplitsXPowSubC (hn : 0 < n) (a : K)
   (rootOfSplits _ (IsSplittingField.splits L (X ^ n - C a))
       (by simpa [degree_X_pow_sub_C hn] using Nat.pos_iff_ne_zero.mp hn))
 
-lemma rootOfSplitsXPowSubC_pow :
-    (rootOfSplitsXPowSubC hn a L) ^ n = algebraMap K L a := by
+lemma rootOfSplitsXPowSubC_pow [NeZero n] :
+    (rootOfSplitsXPowSubC (NeZero.pos n) a L) ^ n = algebraMap K L a := by
   have := map_rootOfSplits _ (IsSplittingField.splits L (X ^ n - C a))
   simp only [eval₂_sub, eval₂_X_pow, eval₂_C, sub_eq_zero] at this
   exact this _
@@ -471,15 +471,15 @@ variable {a}
 roots of unity in `K` if `K` contains all of them.
 Note that this does not depend on a choice of `ⁿ√a`. -/
 noncomputable
-def autEquivRootsOfUnity :
-    (L ≃ₐ[K] L) ≃* (rootsOfUnity ⟨n, hn⟩ K) :=
-  (AlgEquiv.autCongr (adjoinRootXPowSubCEquiv hζ H (rootOfSplitsXPowSubC_pow hn a L)).symm).trans
-    (autAdjoinRootXPowSubCEquiv hζ hn H).symm
-
-lemma autEquivRootsOfUnity_apply_rootOfSplit (σ : L ≃ₐ[K] L) :
-    σ (rootOfSplitsXPowSubC hn a L) =
-      autEquivRootsOfUnity hζ hn H L σ • (rootOfSplitsXPowSubC hn a L) := by
-  obtain ⟨η, rfl⟩ := (autEquivRootsOfUnity hζ hn H L).symm.surjective σ
+def autEquivRootsOfUnity [NeZero n] :
+    (L ≃ₐ[K] L) ≃* (rootsOfUnity n K) :=
+  (AlgEquiv.autCongr (adjoinRootXPowSubCEquiv hζ H (rootOfSplitsXPowSubC_pow a L)).symm).trans
+    (autAdjoinRootXPowSubCEquiv hζ H).symm
+
+lemma autEquivRootsOfUnity_apply_rootOfSplit [NeZero n] (σ : L ≃ₐ[K] L) :
+    σ (rootOfSplitsXPowSubC (NeZero.pos n) a L) =
+      autEquivRootsOfUnity hζ H L σ • (rootOfSplitsXPowSubC (NeZero.pos n) a L) := by
+  obtain ⟨η, rfl⟩ := (autEquivRootsOfUnity hζ H L).symm.surjective σ
   rw [MulEquiv.apply_symm_apply, autEquivRootsOfUnity]
   simp only [MulEquiv.symm_trans_apply, AlgEquiv.autCongr_symm, AlgEquiv.symm_symm,
     MulEquiv.symm_symm, AlgEquiv.autCongr_apply, AlgEquiv.trans_apply,
@@ -488,43 +488,44 @@ lemma autEquivRootsOfUnity_apply_rootOfSplit (σ : L ≃ₐ[K] L) :
   rfl
 
 include hα in
-lemma autEquivRootsOfUnity_smul (σ : L ≃ₐ[K] L) :
-    autEquivRootsOfUnity hζ hn H L σ • α = σ α := by
+lemma autEquivRootsOfUnity_smul [NeZero n] (σ : L ≃ₐ[K] L) :
+    autEquivRootsOfUnity hζ H L σ • α = σ α := by
   have ⟨ζ, hζ'⟩ := hζ
+  have hn := NeZero.pos n
   rw [mem_primitiveRoots hn] at hζ'
   rw [← mem_nthRoots hn, (hζ'.map_of_injective (algebraMap K L).injective).nthRoots_eq
-    (rootOfSplitsXPowSubC_pow hn a L)] at hα
+    (rootOfSplitsXPowSubC_pow a L)] at hα
   simp only [Finset.range_val, Multiset.mem_map, Multiset.mem_range] at hα
   obtain ⟨i, _, rfl⟩ := hα
   simp only [map_mul, ← map_pow, ← Algebra.smul_def, map_smul,
-    autEquivRootsOfUnity_apply_rootOfSplit hζ hn H L]
+    autEquivRootsOfUnity_apply_rootOfSplit hζ H L]
   exact smul_comm _ _ _
 
 /-- Suppose `L/K` is the splitting field of `Xⁿ - a`, and `ζ` is a `n`-th primitive root of unity
 in `K`, then `Gal(L/K)` is isomorphic to `ZMod n`. -/
 noncomputable
-def autEquivZmod {ζ : K} (hζ : IsPrimitiveRoot ζ n) :
+def autEquivZmod [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) :
     (L ≃ₐ[K] L) ≃* Multiplicative (ZMod n) :=
   haveI hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
-  (autEquivRootsOfUnity ⟨ζ, (mem_primitiveRoots hn).mpr hζ⟩ hn H L).trans
-    ((MulEquiv.subgroupCongr (IsPrimitiveRoot.zpowers_eq (k := ⟨n, hn⟩)
+  (autEquivRootsOfUnity ⟨ζ, (mem_primitiveRoots hn).mpr hζ⟩ H L).trans
+    ((MulEquiv.subgroupCongr (IsPrimitiveRoot.zpowers_eq
       (hζ.isUnit_unit' hn)).symm).trans (AddEquiv.toMultiplicative'
         (hζ.isUnit_unit' hn).zmodEquivZPowers.symm))
 
 include hα in
-lemma autEquivZmod_symm_apply_intCast {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℤ) :
+lemma autEquivZmod_symm_apply_intCast [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℤ) :
     (autEquivZmod H L hζ).symm (Multiplicative.ofAdd (m : ZMod n)) α = ζ ^ m • α := by
   have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
-  rw [← autEquivRootsOfUnity_smul ⟨ζ, (mem_primitiveRoots hn).mpr hζ⟩ hn H L hα]
+  rw [← autEquivRootsOfUnity_smul ⟨ζ, (mem_primitiveRoots hn).mpr hζ⟩ H L hα]
   simp [MulEquiv.subgroupCongr_symm_apply, Subgroup.smul_def, Units.smul_def, autEquivZmod]
 
 include hα in
-lemma autEquivZmod_symm_apply_natCast {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℕ) :
+lemma autEquivZmod_symm_apply_natCast [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℕ) :
     (autEquivZmod H L hζ).symm (Multiplicative.ofAdd (m : ZMod n)) α = ζ ^ m • α := by
   simpa only [Int.cast_natCast, zpow_natCast] using autEquivZmod_symm_apply_intCast H L hα hζ m
 
 include hζ H in
-lemma isCyclic_of_isSplittingField_X_pow_sub_C : IsCyclic (L ≃ₐ[K] L) :=
+lemma isCyclic_of_isSplittingField_X_pow_sub_C [NeZero n] : IsCyclic (L ≃ₐ[K] L) :=
   have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
   isCyclic_of_surjective _
     (autEquivZmod H _ <| (mem_primitiveRoots hn).mp hζ.choose_spec).symm.surjective
@@ -641,6 +642,7 @@ lemma isCyclic_tfae (K L) [Field K] [Field L] [Algebra K L] [FiniteDimensional K
       ∃ a : K, Irreducible (X ^ (finrank K L) - C a) ∧
         IsSplittingField K L (X ^ (finrank K L) - C a),
       ∃ (α : L), α ^ (finrank K L) ∈ Set.range (algebraMap K L) ∧ K⟮α⟯ = ⊤] := by
+  have : NeZero (Module.finrank K L) := NeZero.of_pos finrank_pos
   tfae_have 1 → 3
   | ⟨inst₁, inst₂⟩ => exists_root_adjoin_eq_top_of_isCyclic K L hK
   tfae_have 3 → 2

Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

@@ -266,14 +266,16 @@ theorem mem_center_iff {A : SpecialLinearGroup n R} :
     simpa only [coe_mul, ← hr] using (scalar_commute (n := n) r (Commute.all r) B).symm
 
 /-- An equivalence of groups, from the center of the special linear group to the roots of unity. -/
+-- replaced `(Fintype.card n).mkPNat'` by `Fintype.card n` (note `n` is nonempty here)
 @[simps]
 def center_equiv_rootsOfUnity' (i : n) :
-    center (SpecialLinearGroup n R) ≃* rootsOfUnity (Fintype.card n).toPNat' R where
-  toFun A := rootsOfUnity.mkOfPowEq (↑ₘA i i) <| by
-    have : Nonempty n := ⟨i⟩
-    obtain ⟨r, hr, hr'⟩ := mem_center_iff.mp A.property
-    replace hr' : A.val i i = r := by simp [← hr']
-    simp [hr, hr']
+    center (SpecialLinearGroup n R) ≃* rootsOfUnity (Fintype.card n) R where
+  toFun A :=
+    haveI : Nonempty n := ⟨i⟩
+    rootsOfUnity.mkOfPowEq (↑ₘA i i) <| by
+      obtain ⟨r, hr, hr'⟩ := mem_center_iff.mp A.property
+      replace hr' : A.val i i = r := by simp only [← hr', scalar_apply, diagonal_apply_eq]
+      simp only [hr', hr]
   invFun a := ⟨⟨a • (1 : Matrix n n R), by aesop⟩,
     Subgroup.mem_center_iff.mpr fun B ↦ Subtype.val_injective <| by simp [coe_mul]⟩
   left_inv A := by
@@ -294,13 +296,17 @@ open scoped Classical in
 /-- An equivalence of groups, from the center of the special linear group to the roots of unity.
 
 See also `center_equiv_rootsOfUnity'`. -/
+-- replaced `(Fintype.card n).mkPNat'` by what it means, avoiding `PNat`s.
 noncomputable def center_equiv_rootsOfUnity :
-    center (SpecialLinearGroup n R) ≃* rootsOfUnity (Fintype.card n).toPNat' R :=
+    center (SpecialLinearGroup n R) ≃* rootsOfUnity (max (Fintype.card n) 1) R :=
   (isEmpty_or_nonempty n).by_cases
   (fun hn ↦ by
-    rw [center_eq_bot_of_subsingleton, Fintype.card_eq_zero, Nat.toPNat'_zero, rootsOfUnity_one]
+    rw [center_eq_bot_of_subsingleton, Fintype.card_eq_zero, max_eq_right_of_lt zero_lt_one,
+      rootsOfUnity_one]
     exact MulEquiv.mulEquivOfUnique)
-  (fun _ ↦ center_equiv_rootsOfUnity' (Classical.arbitrary n))
+  (fun _ ↦
+    (max_eq_left (NeZero.one_le : 1 ≤ Fintype.card n)).symm ▸
+      center_equiv_rootsOfUnity' (Classical.arbitrary n))
 
 end center
 

Mathlib/NumberTheory/Cyclotomic/Basic.lean

@@ -353,7 +353,7 @@ theorem adjoin_roots_cyclotomic_eq_adjoin_nth_roots [IsDomain B] {ζ : B} {n : 
     rw [IsRoot.def, ← map_cyclotomic n (algebraMap A B), eval_map, ← aeval_def]
     exact hx.2
   · simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hx
-    obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx n.pos
+    obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
     refine SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin ?_) _)
     rw [mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, map_cyclotomic, ← IsRoot]
     exact ⟨cyclotomic_ne_zero n B, hζ.isRoot_cyclotomic n.pos⟩
@@ -362,7 +362,7 @@ theorem adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic {n : ℕ+} [IsDomain B
     (hζ : IsPrimitiveRoot ζ n) : adjoin A ((cyclotomic n A).rootSet B) = adjoin A {ζ} := by
   refine le_antisymm (adjoin_le fun x hx => ?_) (adjoin_mono fun x hx => ?_)
   · suffices hx : x ^ n.1 = 1 by
-      obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx n.pos
+      obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
       exact SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| mem_singleton ζ) _)
     refine (isRoot_of_unity_iff n.pos B).2 ?_
     refine ⟨n, Nat.mem_divisors_self n n.ne_zero, ?_⟩