R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ natDegree (∏ μ in primitiveRoots n R, (X - ↑C μ)) = Nat.totient n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ natDegree (cyclotomic' n R) = Nat.totient n
rw [cyclotomic']
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∑ i in primitiveRoots n R, natDegree (X - ↑C i) = Nat.totient n

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∀ (i : R), i ∈ primitiveRoots n R → X - ↑C i ≠ 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ natDegree (∏ μ in primitiveRoots n R, (X - ↑C μ)) = Nat.totient n
rw [natDegree_prod (primitiveRoots n R) fun z : R => X - C z]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∀ (i : R), i ∈ primitiveRoots n R → X - ↑C i ≠ 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∑ i in primitiveRoots n R, natDegree (X - ↑C i) = Nat.totient n

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∀ (i : R), i ∈ primitiveRoots n R → X - ↑C i ≠ 0
simp only [IsPrimitiveRoot.card_primitiveRoots h, mul_one, natDegree_X_sub_C, Nat.cast_id,
  Finset.sum_const, nsmul_eq_mul]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
z : R
a✝ : z ∈ primitiveRoots n R
⊢ X - ↑C z ≠ 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∀ (i : R), i ∈ primitiveRoots n R → X - ↑C i ≠ 0
intro z _
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
z : R
a✝ : z ∈ primitiveRoots n R
⊢ X - ↑C z ≠ 0
exact X_sub_C_ne_zero z