-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem X_pow_sub_one_eq_prod {ζ : R} {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) :
    X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n R, (X - C ζ)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = (Multiset.map (fun ζ => X - C ζ) (nthRoots n 1)).prod

Tactic:
rw [nthRoots]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = (Multiset.map (fun ζ => X - C ζ) (X ^ n - C 1).roots).prod

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ (X ^ n - C 1).roots.card = (X ^ n - C 1).natDegree

Tactic:
rw [@natDegree_X_pow_sub_C R _ _ n 1, ← nthRoots]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ (nthRoots n 1).card = n

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ (Multiset.map (fun ζ => X - C ζ) (X ^ n - C 1).roots).prod = X ^ n - 1

Tactic:
apply prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmonic

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ (X ^ n - C 1).roots.card = (X ^ n - C 1).natDegree

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ X ^ n - 1 = (Multiset.map (fun ζ => X - C ζ) (X ^ n - C 1).roots).prod

Tactic:
symm

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ (Multiset.map (fun ζ => X - C ζ) (X ^ n - C 1).roots).prod = X ^ n - 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ ∈ { val := nthRoots n 1, nodup := ⋯ }, (X - C ζ)

Tactic:
simp only [Finset.prod_mk, RingHom.map_one]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = (Multiset.map (fun ζ => X - C ζ) (nthRoots n 1)).prod

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n R, (X - C ζ)

Tactic:
rw [nthRootsFinset, ← Multiset.toFinset_eq (IsPrimitiveRoot.nthRoots_one_nodup h)]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ ∈ { val := nthRoots n 1, nodup := ⋯ }, (X - C ζ)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ (nthRoots n 1).card = n

Tactic:
exact IsPrimitiveRoot.card_nthRoots_one h

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = (Multiset.map (fun ζ => X - C ζ) (X ^ n - C 1).roots).prod

Tactic:
have hmonic : (X ^ n - C (1 : R)).Monic := monic_X_pow_sub_C (1 : R) (ne_of_lt hpos).symm

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ X ^ n - 1 = (Multiset.map (fun ζ => X - C ζ) (X ^ n - C 1).roots).prod

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n R, (X - C ζ)

Tactic:
classical
rw [nthRootsFinset, ← Multiset.toFinset_eq (IsPrimitiveRoot.nthRoots_one_nodup h)]
simp only [Finset.prod_mk, RingHom.map_one]
rw [nthRoots]
have hmonic : (X ^ n - C (1 : R)).Monic := monic_X_pow_sub_C (1 : R) (ne_of_lt hpos).symm
symm
apply prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmonic
rw [@natDegree_X_pow_sub_C R _ _ n 1, ← nthRoots]
exact IsPrimitiveRoot.card_nthRoots_one h

Result:
no goals