@@ -65,24 +65,22 @@ theorem contains_two_primitive_roots {p q : ℕ} {x y : K} [FiniteDimensional
6565 have hkpos : 0 < k := Nat.pos_of_ne_zero (Nat.lcm_ne_zero hppos.ne' hqpos.ne')
6666 let xu := IsUnit.unit (hx.isUnit hppos)
6767 let yu := IsUnit.unit (hy.isUnit hqpos)
68- have hxmem : xu ∈ rootsOfUnity ⟨k, hkpos⟩ K := by
69- rw [mem_rootsOfUnity, PNat.mk_coe, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
70- IsUnit.unit_spec]
68+ have hxmem : xu ∈ rootsOfUnity k K := by
69+ rw [mem_rootsOfUnity, ← Units.val_eq_one, Units.val_pow_eq_pow_val, IsUnit.unit_spec]
7170 exact (hx.pow_eq_one_iff_dvd _).2 (dvd_lcm_left _ _)
72- have hymem : yu ∈ rootsOfUnity ⟨k, hkpos⟩ K := by
73- rw [mem_rootsOfUnity, PNat.mk_coe, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
74- IsUnit.unit_spec]
71+ have hymem : yu ∈ rootsOfUnity k K := by
72+ rw [mem_rootsOfUnity, ← Units.val_eq_one, Units.val_pow_eq_pow_val, IsUnit.unit_spec]
7573 exact (hy.pow_eq_one_iff_dvd _).2 (dvd_lcm_right _ _)
76- have hxuord : orderOf (⟨xu, hxmem⟩ : rootsOfUnity ⟨k, hkpos⟩ K) = p := by
77- rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
74+ have hxuord : orderOf (⟨xu, hxmem⟩ : rootsOfUnity k K) = p := by
75+ rw [← orderOf_injective (rootsOfUnity k K).subtype Subtype.coe_injective,
7876 Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, IsUnit.unit_spec]
7977 exact hx.eq_orderOf.symm
80- have hyuord : orderOf (⟨yu, hymem⟩ : rootsOfUnity ⟨k, hkpos⟩ K) = q := by
81- rw [← orderOf_injective (rootsOfUnity ⟨k, hkpos⟩ K).subtype Subtype.coe_injective,
78+ have hyuord : orderOf (⟨yu, hymem⟩ : rootsOfUnity k K) = q := by
79+ rw [← orderOf_injective (rootsOfUnity k K).subtype Subtype.coe_injective,
8280 Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, IsUnit.unit_spec]
8381 exact hy.eq_orderOf.symm
84- obtain ⟨g : rootsOfUnity ⟨k, hkpos⟩ K, hg⟩ :=
85- IsCyclic.exists_monoid_generator (α := rootsOfUnity ⟨k, hkpos⟩ K)
82+ have : NeZero k := ⟨hkpos.ne'⟩
83+ obtain ⟨g : rootsOfUnity k K, hg⟩ := IsCyclic.exists_monoid_generator (α := rootsOfUnity k K)
8684 obtain ⟨nx, hnx⟩ := hg ⟨xu, hxmem⟩
8785 obtain ⟨ny, hny⟩ := hg ⟨yu, hymem⟩
8886 have H : orderOf g = k := by
@@ -123,7 +121,7 @@ theorem IsPrimitiveRoot.eq_one_mod_sub_of_pow {A : Type*} [CommRing A] [IsDomain
123121 (hζ : IsPrimitiveRoot ζ p) {μ : A} (hμ : μ ^ (p : ℕ) = 1 ) :
124122 (@DFunLike.coe _ A (fun _ => A ⧸ Ideal.span {ζ - 1 }) _
125123 (algebraMap A (A ⧸ Ideal.span {ζ - 1 })) μ) = 1 := by
126- obtain ⟨k, -, rfl⟩ := hζ.eq_pow_of_pow_eq_one hμ p.pos
124+ obtain ⟨k, -, rfl⟩ := hζ.eq_pow_of_pow_eq_one hμ
127125 rw [map_pow, eq_one_mod_one_sub, one_pow]
128126
129127set_option synthInstance.maxHeartbeats 80000 in
@@ -232,7 +230,7 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K)
232230 simp only [one_pow]
233231 apply hxp'
234232 cases' hxp'' with hxp'' hxp''
235- · obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp'' p.prop
233+ · obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp''
236234 refine ⟨i, 2 , ?_⟩
237235 rw [← Subtype.val_inj] at Hi
238236 simp only [SubmonoidClass.coe_pow] at Hi
@@ -243,7 +241,7 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K)
243241 have hxp3 : (-1 * ⟨x, hx⟩ : R) ^ (p : ℕ) = 1 := by
244242 rw [mul_pow, hone, hxp'']
245243 ring
246- obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp3 p.prop
244+ obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp3
247245 refine ⟨i, 1 , ?_⟩
248246 simp only [PNat.one_coe, pow_one, neg_mul, one_mul, neg_neg]
249247 rw [← Subtype.val_inj] at Hi
@@ -376,5 +374,5 @@ theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u :
376374lemma IsPrimitiveRoot.eq_one_mod_one_sub' {A : Type *} [CommRing A] [IsDomain A]
377375 {n : ℕ+} {ζ : A} (hζ : IsPrimitiveRoot ζ n) {η : A} (hη : η ∈ nthRootsFinset n A) :
378376 Ideal.Quotient.mk (Ideal.span ({ζ - 1 } : Set A)) η = 1 := by
379- obtain ⟨i, ⟨_, rfl⟩⟩ := hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset n.2 ).1 hη) n. 2
377+ obtain ⟨i, ⟨_, rfl⟩⟩ := hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset n.2 ).1 hη)
380378 rw [map_pow, ← Ideal.Quotient.algebraMap_eq, eq_one_mod_one_sub, one_pow]
0 commit comments