n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ degree (map (Int.castRingHom R) (cyclotomic n ℤ)) = ↑(Nat.totient n)
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ degree (cyclotomic n R) = ↑(Nat.totient n)
rw [← map_cyclotomic_int]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ degree (cyclotomic n ℤ) = ↑(Nat.totient n)

n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ ↑(Int.castRingHom R) (leadingCoeff (cyclotomic n ℤ)) ≠ 0
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ degree (map (Int.castRingHom R) (cyclotomic n ℤ)) = ↑(Nat.totient n)
rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom R) _]
no goals
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ ↑(Int.castRingHom R) (leadingCoeff (cyclotomic n ℤ)) ≠ 0
simp only [(int_cyclotomic_spec n).right.right, eq_intCast, Monic.leadingCoeff, Int.cast_one,
  Ne.def, not_false_iff, one_ne_zero]
case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ degree (cyclotomic Nat.zero ℤ) = ↑(Nat.totient Nat.zero)

case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
k : ℕ
⊢ degree (cyclotomic (Nat.succ k) ℤ) = ↑(Nat.totient (Nat.succ k))
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ degree (cyclotomic n ℤ) = ↑(Nat.totient n)
cases' n with k
case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
k : ℕ
⊢ degree (cyclotomic (Nat.succ k) ℤ) = degree (cyclotomic' (Nat.succ k) ℂ)
case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
k : ℕ
⊢ degree (cyclotomic (Nat.succ k) ℤ) = ↑(Nat.totient (Nat.succ k))
rw [← degree_cyclotomic' (Complex.isPrimitiveRoot_exp k.succ (Nat.succ_ne_zero k))]
no goals
case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
k : ℕ
⊢ degree (cyclotomic (Nat.succ k) ℤ) = degree (cyclotomic' (Nat.succ k) ℂ)
exact (int_cyclotomic_spec k.succ).2.1
no goals
case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ degree (cyclotomic Nat.zero ℤ) = ↑(Nat.totient Nat.zero)
simp only [cyclotomic, degree_one, dif_pos, Nat.totient_zero, WithTop.coe_zero]