R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ in { val := nthRoots n 1, nodup := (_ : Multiset.Nodup (nthRoots n 1)) }, (X - ↑C ζ)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ in nthRootsFinset n R, (X - ↑C ζ)
rw [nthRootsFinset, ← Multiset.toFinset_eq (IsPrimitiveRoot.nthRoots_nodup h)]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = Multiset.prod (Multiset.map (fun x => X - ↑C x) (nthRoots n 1))
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ in { val := nthRoots n 1, nodup := (_ : Multiset.Nodup (nthRoots n 1)) }, (X - ↑C ζ)
simp only [Finset.prod_mk, RingHom.map_one]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots (X ^ n - ↑C 1)))
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = Multiset.prod (Multiset.map (fun x => X - ↑C x) (nthRoots n 1))
rw [nthRoots]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : Monic (X ^ n - ↑C 1)
⊢ X ^ n - 1 = Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots (X ^ n - ↑C 1)))
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots (X ^ n - ↑C 1)))
have hmonic : (X ^ n - C (1 : R)).Monic := monic_X_pow_sub_C (1 : R) (ne_of_lt hpos).symm
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : Monic (X ^ n - ↑C 1)
⊢ Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots (X ^ n - ↑C 1))) = X ^ n - 1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : Monic (X ^ n - ↑C 1)
⊢ X ^ n - 1 = Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots (X ^ n - ↑C 1)))
symm
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : Monic (X ^ n - ↑C 1)
⊢ ↑Multiset.card (roots (X ^ n - ↑C 1)) = natDegree (X ^ n - ↑C 1)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : Monic (X ^ n - ↑C 1)
⊢ Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots (X ^ n - ↑C 1))) = X ^ n - 1
apply prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmonic
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : Monic (X ^ n - ↑C 1)
⊢ ↑Multiset.card (nthRoots n 1) = n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : Monic (X ^ n - ↑C 1)
⊢ ↑Multiset.card (roots (X ^ n - ↑C 1)) = natDegree (X ^ n - ↑C 1)
rw [@natDegree_X_pow_sub_C R _ _ n 1, ← nthRoots]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : Monic (X ^ n - ↑C 1)
⊢ ↑Multiset.card (nthRoots n 1) = n
exact IsPrimitiveRoot.card_nthRoots h